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.
Type de document :
Communication dans un congrès
SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. SETS14, 1st International Workshop about Sets and Tools, 2014, Toulouse, France, EasyChair., pp.12, 2014, 〈http://sets2014.cnam.fr/〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01100512
Contributeur : Pierre Halmagrand <>
Soumis le : mardi 6 janvier 2015 - 15:23:13
Dernière modification le : jeudi 13 septembre 2018 - 15:24:05
Document(s) archivé(s) le : mercredi 3 juin 2015 - 17:25:43

Fichier

zen-mod.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. SETS14, 1st International Workshop about Sets and Tools, 2014, Toulouse, France, EasyChair., pp.12, 2014, 〈http://sets2014.cnam.fr/〉. 〈hal-01100512〉

Partager

Métriques

Consultations de la notice

251

Téléchargements de fichiers

96