Superposition for full higher-order logic
type: Item
instance of: scholarly article
title: Superposition for full higher-order logic
zbMATH Open document ID: 1497.03030
DOI: 10.1007/978-3-030-79876-5_23
author: Alexander Bentkamp
author: Jasmin Christian Blanchette
author: Sophie Tourret
author: Petar Vukmirović
publication date: 2021-12-01T00:00:00Z
review text: Superposition [\textit{L. Bachmair} and \textit{H. Ganzinger}, J. Log. Comput. 4, No. 3, 217--247 (1994; Zbl 0814.68117)] is a state-of-the-art inference system for automated theorem proving in classical first-order logic with equality. The problem of extending superposition to variants of classical higher-order logic has recently been gaining increasing attention. The authors essentially combine earlier work on superposition with Booleans [\textit{V. Nummelin} et al., Lect. Notes Comput. Sci. 12699, 378--395 (2021; Zbl 07437090)] and Boolean-free \(\lambda\)-superposition [\textit{A. Bentkamp} et al., J. Autom. Reasoning 65, No. 7, 893--940 (2021; Zbl 07433023)] to obtain a sound and refutationally complete superposition calculus for full rank-1 polymorphic classical higher-order logic which includes both Booleans and \(\lambda\)-expressions. A proof of refutational completeness is briefly sketched, with the details delegated to a technical report. The authors describe the implementation of their superposition calculus in the Zipperposition prover [\textit{S. Cruanes}, Lect. Notes Comput. Sci. 10483, 172--188 (2017; Zbl 1496.68365)] and provide an experimental evaluation. The implementation outperforms all other higher-order theorem provers. For the entire collection see [Zbl 1475.68026].
reviewed by: Łukasz Czajka
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B16
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437091
zbMATH Keywords: superposition
zbMATH Keywords: higher-order logic
zbMATH Keywords: Booleans
describes a project that uses: Zipperposition
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 23
OpenAlex ID: W3180051810
cites work: On connections and higher-order logic
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Superposition with lambdas
cites work: Superposition for \(\lambda\)-free higher-order logic
cites work: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
cites work: A combinator-based superposition calculus for higher-order logic
cites work: Sledgehammer: Judgement Day
cites work: Satallax: An Automatic Higher-Order Prover
cites work: Types, tableaus, and Gödel's God
cites work: Superposition with equivalence reasoning and delayed clause normal form transformation
cites work: Q5287513
cites work: Mechanizing \(\omega\)-order type theory through unification
cites work: An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
cites work: Superposition with first-class booleans and inprocessing clausification
cites work: Q3150301
cites work: The higher-order prover Leo-III
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: Making higher-order superposition work
cites work: A comprehensive framework for saturation theorem proving
cites work: Simultaneous paramodulation
description: scientific article; zbMATH DE number 7437091