Superposition for full higher-order logic

DOI10.1007/978-3-030-79876-5_23zbMath1497.03030OpenAlexW3180051810MaRDI QIDQ2055874

Jasmin Christian Blanchette, Alexander Bentkamp, Sophie Tourret, Petar Vukmirović

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_23

zbMATH Keywords

higher-order logicsuperpositionBooleans

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (11)

The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Superposition for higher-order logic ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Superposition for full higher-order logic ⋮ A comprehensive framework for saturation theorem proving ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• Zipperposition

Cites Work

• Unnamed Item
• Unnamed Item
• On connections and higher-order logic
• Mechanizing \(\omega\)-order type theory through unification
• Types, tableaus, and Gödel's God
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Superposition for \(\lambda\)-free higher-order logic
• The higher-order prover Leo-III
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• A combinator-based superposition calculus for higher-order logic
• Superposition with equivalence reasoning and delayed clause normal form transformation
• Satallax: An Automatic Higher-Order Prover
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Sledgehammer: Judgement Day
• Superposition with lambdas
• Making higher-order superposition work
• A comprehensive framework for saturation theorem proving

This page was built for publication: Superposition for full higher-order logic