Hierarchic Superposition With Weak Abstraction

Abstract : Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide a new completeness result for the fragment where all background-sorted terms are ground.
Type de document :
Communication dans un congrès
Maria Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.39-57, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00931919
Contributeur : Stephan Merz <>
Soumis le : jeudi 16 janvier 2014 - 09:47:07
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Lien texte intégral

Identifiants

Collections

Citation

Peter Baumgartner, Uwe Waldmann. Hierarchic Superposition With Weak Abstraction. Maria Paola Bonacina. 24th International Conference on Automated Deduction (CADE-24), Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.39-57, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38574-2_3〉. 〈hal-00931919〉

Partager

Métriques

Consultations de la notice

157