A modular formalization of superposition in Isabelle/HOL
From MaRDI portal
Cites work
- A combinator-based superposition calculus for higher-order logic
- A comprehensive framework for saturation theorem proving
- A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
- A Machine-Oriented Logic Based on the Resolution Principle
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- A sequent calculus for first-order logic formalized in Isabelle/HOL
- A verified decision procedure for orders in Isabelle/HOL
- A verified SAT solver framework with learn, forget, restart, and incrementality
- An Isabelle/HOL Formalization of the SCL(FOL) Calculus
- Certification of Termination Proofs Using CeTA
- Faster, higher, stronger: E 2.3
- Formalizing a Seligman-style tableau system for hybrid logic (short paper)
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Hierarchic superposition revisited
- scientific article; zbMATH DE number 1300967 (Why is no real title available?)
- scientific article; zbMATH DE number 1301853 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Metamathematics, Machines and Gödel's Proof
- On restrictions of ordered paramodulation with simplification
- Resolution theorem proving
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- SCL clause learning from simple models
- Superposition for higher-order logic
- Superposition for lambda-free higher-order logic
- Superposition with lambdas
- Superposition with Delayed Unification
Cited in
(4)
This page was built for publication: A modular formalization of superposition in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860021)
