[Termtools] termination competition changes

[Johannes Waldmann]

For the semantics of pre-defined modules (integer and possibly others)
I suggest to investigate how to re-use
the design and documentation effort that already went into SMT-LIB,
see http://combination.cs.uiowa.edu/smtlib/

(Especially since Fixed_Size_Bitvectors
were mentioned already mentioned here).

It seems STM-LIB has no provision for combination of modules
(all of their theories seem mono-sorted).

PS: I think Booleans do not belong into Integer. SMT-LIB of course
avoids this problem because they have truth values "for free".

Johannes.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20090225/1585f109/attachment.pgp