Superposition with first-class booleans and inprocessing clausification
From MaRDI portal
Publication:2055873
DOI10.1007/978-3-030-79876-5_22OpenAlexW3181451889MaRDI QIDQ2055873FDOQ2055873
Authors: Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirović 
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_22
Recommendations
- Superposition for higher-order logic
- Superposition for full higher-order logic
- Semantics for first-order superposition logic
- On the superposition of Boolean functions
- scientific article; zbMATH DE number 7350767
- Superposition for \(\lambda\)-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
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Why3 -- where programs meet provers
- Faster, higher, stronger: E 2.3
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Resolution theorem proving
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Title not available (Why is that?)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Title not available (Why is that?)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- AVATAR: The Architecture for First-Order Theorem Provers
- Computing small clause normal forms
- A Deductive Approach to Program Synthesis
- Completely non-clausal theorem proving
- Superposition with structural induction
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Superposition for bounded domains
- Hierarchic superposition with weak abstraction
- Title not available (Why is that?)
- Superposition with datatypes and codatatypes
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- Superposition with equivalence reasoning and delayed clause normal form transformation
- A comprehensive framework for saturation theorem proving
- Simultaneous paramodulation
Cited In (6)
- Set of support, demodulation, paramodulation: a historical perspective
- AC simplifications and closure redundancies in the superposition calculus
- Making higher-order superposition work
- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- A comprehensive framework for saturation theorem proving
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)
