Certification of Completion Results
The certification of results can also be replayed using the checker extracted from the Coq
theory. Once it is compiled, the checher can be runned on a comp.res file (produce by Timbuk
while running completion). Given a TRS and
two tree automata Ainit and Acomp, the checker verifies that
L(Acomp) contains L(Ainit) and that L(Acomp) is closed by rewriting.
This proves that L(Acomp) is a superset of R*(L(Ainit)). For details
about the theory see this paper.
On all the examples of this page the checker takes only a few
milliseconds to certify the restult.
If we run
checker -fp comp.res
we obtain the following output if the certification succeeds:
Post fixpoint :
- R1*(Ainit) included in Acomp : OK
Otherwise, if the verification fails, the output is of the form:
Post fixpoint :
- R1*(Ainit) included in Acomp : KO