Superposition for Lambda-Free Higher-Order Logic

Abstract : We introduce refutationally complete superposition calculi for intentional and extensional λ-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the λ-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.
Type de document :
Communication dans un congrès
IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées

https://hal.inria.fr/hal-01904595
Contributeur : Jasmin Christian Blanchette <>
Soumis le : jeudi 25 octobre 2018 - 10:45:50
Dernière modification le : mercredi 7 novembre 2018 - 15:19:40

Fichier

lfhosup_paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01904595, version 1

Collections

Citation

Alexander Bentkamp, Simon Cruanes, Jasmin Christian Blanchette, Uwe Waldmann. Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. 〈hal-01904595〉

Partager

Métriques

Consultations de la notice

47

Téléchargements de fichiers

5