[Termtools] certified - strange proofs
Christian Sternagel
christian.sternagel at uibk.ac.at
Wed Jun 6 10:21:37 CEST 2007
It seems as there was a second missunderstanding between me and the
Rainbow(runscript)-authors. I assumed that everything except a
correct XML-file is interpreted as a wrong proof. But I saw
that everytime when ttt2-cert outputs `MAYBE' (instead of an XML-file)
there is a YES in the coq-proof output followed by an exception.
The real strange thing is, that Coq afterwards succeeds in certifying,
but there is no proof at all.
An example is: TRS/SK90/2.26.trs
cheers
christian
More information about the Termtools
mailing list