Certifying a Termination Criterion Based on Graphs, without Graphs

Although graphs are very common in computer science, they are still very difficult to handle for proof assistants as proving properties of graphs may require heavy computations. This is a problem when it comes to issues such as the certification of a proof of well-foundedness, since premises of generic theorems involving graph properties may be at least as difficult to prove as their conclusion. We define a framework and propose an original approach based on both shallow and deep embeddings for the mechanical certification of these kinds of proofs without the help of any graph library. This framework actually avoids concrete models of graphs and handles those implicitly. We illustrate this approach on a powerful refinement of the dependency pairs approach for proving termination. This refinement makes heavy use of graph analysis and our technique is powerful enough to deal efficiently –and with full automation– with graphs containing thousands of arcs, as they may occur in ...

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Pierre Courtieu, Julien Forest, Xavier Urbain
• Keywords: Artificial Intelligence, Heavy Computations, Proof Assistants, Theorems Involving Graph, TPHOL 2008