A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms

Abstract : We generalize the Knuth-Bendix order (KBO) to higher-order terms without λ-abstraction. The restriction of this new order to first-order terms coincides with the traditional KBO. The order has many useful properties, including transitivity, the subterm property, compatibility with contexts (monotonicity), stability under substitution, and well-foundedness. Transfinite weights and argument coefficients can also be supported. The order appears promising as the basis of a higher-order superposition calculus.
Type de document :
Communication dans un congrès
Leonardo de Moura. CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.432-453, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_27〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01592186
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 septembre 2017 - 18:48:24
Dernière modification le : mardi 30 janvier 2018 - 16:38:02
Document(s) archivé(s) le : jeudi 28 décembre 2017 - 12:40:00

Fichier

BeckerBlanchetteWaldmannWandCA...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Heiko Becker, Jasmin Blanchette, Uwe Waldmann, Daniel Wand. A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. Leonardo de Moura. CADE-26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.432-453, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_27〉. 〈hal-01592186〉

Partager

Métriques

Consultations de la notice

150

Téléchargements de fichiers

38