Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation

Harald Ganzinger 1 Jürgen Stuber 2
1 MPII - Max-Planck-Institut für Informatik
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The paper presents a completeness proof and reports on practical experience obtained with the Saturate system.
keyword : calcul de superposition superposition calculus superposition simplification
Type de document :
Communication dans un congrès
Franz Baader. 19th International Conference on Automated Deduction - CADE-19, 2003, Miami Beach, FL, United States. Springer Berlin / Heidelberg, 2741, pp.335-349, 2003, Lecture notes in Computer Science. 〈10.1007/978-3-540-45085-6_31〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00099710
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:40:30
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Harald Ganzinger, Jürgen Stuber. Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. Franz Baader. 19th International Conference on Automated Deduction - CADE-19, 2003, Miami Beach, FL, United States. Springer Berlin / Heidelberg, 2741, pp.335-349, 2003, Lecture notes in Computer Science. 〈10.1007/978-3-540-45085-6_31〉. 〈inria-00099710〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

67

Contact


archive-ouverte@inria.fr