Superposition for full higher-order logic

DOI10.1007/978-3-030-79876-5_23zbMATH Open1497.03030OpenAlexW3180051810MaRDI QIDQ2055874FDOQ2055874

Authors: Alexander Bentkamp, Jasmin Christian Blanchette, 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

Recommendations

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

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)

Cites Work

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

Cited In (25)

• SAT-Inspired Higher-Order Eliminations
• Solving modal logic problems by translation to higher-order logic
• Superposition with lambdas
• Set of support, demodulation, paramodulation: a historical perspective
• 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
• 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
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work
• Superposition with first-class booleans and inprocessing clausification
• Superposition for full higher-order logic
• Superposition for \(\lambda\)-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

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)