zbMATH — the first resource for mathematics

Superposition for \(\lambda\)-free higher-order logic. (English) Zbl 06958090
Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-94204-9/pbk; 978-3-319-94205-6/ebook). Lecture Notes in Computer Science 10900. Lecture Notes in Artificial Intelligence, 28-46 (2018).
Summary: We introduce refutationally complete superposition calculi for intentional and extensional \(\lambda\)-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 \(\lambda\)-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.
For the entire collection see [Zbl 1391.68006].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI