HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Using Deduction Modulo in Set Theory

Abstract : We present some improvements of Zenon Modulo and the application of this tool to sets of problems coming from set theory. Zenon Modulo is an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. Deduction modulo is an ex-tension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well-suited for proof-search in axiomatic theories, as it turns axioms into rewrite rules. The improvements dis-cussed here consist in a better heuristic to automatically build rewrite systems given a set of axioms, and some optimizations in the rewrit-ing process used during the proof search. We also present some updated results obtained on benchmarks provided by the TPTP library for set theory categories. Finally, we discuss some recent work about the appli-cation of our tool to the B method set theory, in particular the way we treat equality and the comprehension scheme.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

Contributor : Pierre Halmagrand Connect in order to contact the contributor
Submitted on : Tuesday, January 6, 2015 - 3:23:13 PM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
Long-term archiving on: : Wednesday, June 3, 2015 - 5:25:43 PM


Files produced by the author(s)


  • HAL Id : hal-01100512, version 1



Pierre Halmagrand. Using Deduction Modulo in Set Theory. SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. pp.12. ⟨hal-01100512⟩



Record views


Files downloads