First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice

Abstract : We discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with the introduction of a rewrite feature. Deduction modulo theory is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We introduce two automated reasoning systems that have been built to extend other provers with Deduction modulo theory. The first one is Zenon Modulo, a tableau-based tool able to deal with polymorphic first-order logic with equality, while the second one is iProverModulo, a resolution-based system dealing with first-order logic with equality. We also provide some experimental results run on benchmarks that show the beneficial impact of the extension on these two tools and their underlying proof search methods. Finally, we describe the two backends of these systems to the Dedukti universal proof checker, which also relies on Deduction modulo theory, and which allows us to verify the proofs produced by these tools.
Document type :
Journal articles
Complete list of metadatas

Cited literature [112 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02305831
Contributor : Guillaume Burel <>
Submitted on : Thursday, October 17, 2019 - 11:06:54 AM
Last modification on : Thursday, October 17, 2019 - 4:00:47 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2020-03-23

Please log in to resquest access to the document

Identifiers

Citation

Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, et al.. First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. Journal of Automated Reasoning, Springer Verlag, In press, ⟨10.1007/s10817-019-09533-z⟩. ⟨hal-02305831⟩

Share

Metrics

Record views

79