[Termtools] Naive comments from an occasional visitor

[Johannes Waldmann]

One comment on Matchbox (also using Color):

Matchbox does not know polynomial interpretations.
It has linear interpretations (treated as 1-dimensional
matrix interpretations) but no mixed polynomials,
and consequently loses some proofs w.r.t. Aprove/Color.

For the methods that are in common, Aprove's proof search
(constraint solving) is working better. It seems Matchbox
is wasting time generating too many subprocesses.

best regards, J.W.

-------------- 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/20081110/38499ff1/attachment.pgp