Hierarchic Superposition: Completeness without Compactness

Abstract : Many applications of automated deduction and verification require reasoning in combinations of theories, such as, on the one hand (some fragment of) first-order logic, and on, the other hand a background theory, such as some form of arithmetic. Unfortunately, due to the high expressivity of the full logic, complete reasoning is impossible in general. It is a realistic goal, however, to devise theorem provers that are "reasonably complete" in practice, and the hierarchic superposition calculus has been designed as a theoretical basis for that. In a recent paper we introduced an extension of hierarchic superposition and proved its completeness for the fragment where every term of the background sort is ground. In this paper, we extend this result and obtain completeness for a larger fragment that admits variables in certain places.
Type de document :
Communication dans un congrès
Marek Kosta and Thomas Sturm. MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12, 〈http://resources.mpi-inf.mpg.de/conferences/macis2013/program.html〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01087872
Contributeur : Stephan Merz <>
Soumis le : jeudi 27 novembre 2014 - 02:54:40
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

  • HAL Id : hal-01087872, version 1

Collections

Citation

Peter Baumgartner, Uwe Waldmann. Hierarchic Superposition: Completeness without Compactness. Marek Kosta and Thomas Sturm. MACIS 2013 - Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, Dec 2013, Nanning, China. pp.8-12, 〈http://resources.mpi-inf.mpg.de/conferences/macis2013/program.html〉. 〈hal-01087872〉

Partager

Métriques

Consultations de la notice

232