Superposition with first-class booleans and inprocessing clausification
From MaRDI portal
Publication:2055873
DOI10.1007/978-3-030-79876-5_22OpenAlexW3181451889MaRDI QIDQ2055873
Sophie Tourret, Visa Nummelin, Alexander Bentkamp, Petar Vukmirović
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_22
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
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 ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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 with datatypes and codatatypes
- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- Faster, higher, stronger: E 2.3
- Superposition with equivalence reasoning and delayed clause normal form transformation
- AVATAR: The Architecture for First-Order Theorem Provers
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Solving SAT and SAT Modulo Theories
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- A Deductive Approach to Program Synthesis
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Superposition for Bounded Domains
- Hierarchic Superposition with Weak Abstraction
- Why3 — Where Programs Meet Provers
- A comprehensive framework for saturation theorem proving
This page was built for publication: Superposition with first-class booleans and inprocessing clausification
