Superposition for higher-order logic

DOI10.1007/S10817-022-09649-9MaRDI QIDQ6156638zbMATH OpenOpenAlexFDO

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

Publication date 14 June 2023

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-022-09649-9

zbMATH Keywords

higher-order logicrefutational completenesssuperposition calculus

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A combinator-based superposition calculus for higher-order logic
• A comprehensive framework for saturation theorem proving
• A Linear Spine Calculus
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Computing small clause normal forms
• Higher-order rewrite systems and their confluence
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Making higher-order superposition work
• Mechanizing \(\omega\)-order type theory through unification
• On connections and higher-order logic
• Resolution theorem proving
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Satallax: An Automatic Higher-Order Prover
• Simultaneous paramodulation
• Sledgehammer: judgement day
• Superposition for full higher-order logic
• Superposition for lambda-free higher-order logic
• Superposition with equivalence reasoning and delayed clause normal form transformation
• Superposition with lambdas
• The computability path ordering
• The higher-order prover Leo-III
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Types, tableaus, and Gödel's God

Cited in

(12)

• Superposition with first-class booleans and inprocessing clausification
• Implementing Superposition in iProver (System Description)
• Super logic programs
• Hammering Floating-Point Arithmetic
• A modular formalization of superposition in Isabelle/HOL
• Duper: a proof-producing superposition theorem prover for dependent type theory
• Notes on Gödel's and Scott's variants of the ontological argument
• Experiments with choice in dependently-typed higher-order logic
• Automatic bit- and memory-precise verification of eBPF code
• Tableaux for automated reasoning in dependently-typed higher-order logic
• A higher-order Vampire (short paper)
• Automated reasoning for mathematics

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6156638)