Superposition with first-class booleans and inprocessing clausification
From MaRDI portal
Recommendations
- Superposition for higher-order logic
- Superposition for full higher-order logic
- Semantics for first-order superposition logic
- On the superposition of Boolean functions
- Superposition for lambda-free higher-order logic
- Superposition for -free higher-order logic
- Propositional superposition logic
- Classes of functions of multi-valued logic closed with respect to superposition and inversion operations
- Completion of first-order clauses with equality by strict superposition
- A combinator-based superposition calculus for higher-order logic
Cites work
- A comprehensive framework for saturation theorem proving
- A Deductive Approach to Program Synthesis
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- AVATAR: The Architecture for First-Order Theorem Provers
- Completely non-clausal theorem proving
- Computing small clause normal forms
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Faster, higher, stronger: E 2.3
- Hierarchic superposition with weak abstraction
- scientific article; zbMATH DE number 1324442 (Why is no real title available?)
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Resolution theorem proving
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Simultaneous paramodulation
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Superposition for bounded domains
- Superposition for full higher-order logic
- Superposition with datatypes and codatatypes
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Superposition with first-class booleans and inprocessing clausification
- Superposition with structural induction
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Why3 -- where programs meet provers
Cited in
(7)- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- Set of support, demodulation, paramodulation: a historical perspective
- AC simplifications and closure redundancies in the superposition calculus
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
Describes a project that uses
Uses Software
This page was built for publication: Superposition with first-class booleans and inprocessing clausification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055873)
