Superposition for full higher-order logic

DOI10.1007/978-3-030-79876-5_23MaRDI QIDQ2055874zbMATH OpenOpenAlexFDO

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

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

superpositionhigher-order logicBooleans

Mathematics Subject Classification ID

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

Recommendations

• Making higher-order superposition work
• Superposition for -free higher-order logic
• Making higher-order superposition work
• Superposition with lambdas
• Superposition and Model Evolution Combined

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A combinator-based superposition calculus for higher-order logic
• A comprehensive framework for saturation theorem proving
• 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)
• Making higher-order superposition work
• Mechanizing \(\omega\)-order type theory through unification
• On connections and higher-order logic
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Satallax: An Automatic Higher-Order Prover
• Simultaneous paramodulation
• Sledgehammer: judgement day
• Superposition for -free higher-order logic
• Superposition for full higher-order logic
• Superposition with equivalence reasoning and delayed clause normal form transformation
• Superposition with first-class booleans and inprocessing clausification
• Superposition with lambdas
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The higher-order prover Leo-III
• Types, tableaus, and Gödel's God

Cited in

(26)

• Set of support, demodulation, paramodulation: a historical perspective
• Superposition with lambdas
• SAT-Inspired Higher-Order Eliminations
• Solving modal logic problems by translation to higher-order logic
• Superposition as a logical glue
• Semantics for first-order superposition logic
• Superposition with structural induction
• Superposition and Model Evolution Combined
• A complete superposition calculus for primal grammars
• Making higher-order superposition work
• Superposition with lambdas
• Set-of-support strategy for higher-order logic
• Superposition for higher-order logic
• Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work
• Superposition for -free higher-order logic
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• A comprehensive framework for saturation theorem proving
• Verified Given Clause Procedures
• Higher-order superposition for dependent types
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Extending a high-performance prover to higher-order logic
• Beagle -- a hierarchic superposition theorem prover

Describes a project that uses

Uses Software

• Zipperposition

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

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