[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