Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Certifying a Termination Criterion Based on Graphs, without Graphs
verfasst von : Pierre Courtieu, Julien Forest, Xavier Urbain
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 practice.