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

https://hal.inria.fr/hal-01100512
Contributor : Pierre Halmagrand <>
Submitted on : Tuesday, January 6, 2015 - 3:23:13 PM
Last modification on : Tuesday, December 8, 2020 - 9:44:10 AM
Long-term archiving on: : Wednesday, June 3, 2015 - 5:25:43 PM

File

zen-mod.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01100512, version 1

Collections

Citation

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

Share

Metrics

Record views

346

Files downloads

261