SAT-Inspired Eliminations for Superposition

DOI10.1145/3565366OpenAlexW4298140626MaRDI QIDQ5875949

Petar Vukmirović, Marijn J. H. Heule, Jasmin Christian Blanchette

Publication date: 7 February 2023

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3565366

zbMATH Keywords

theorem provingfirst-order logicSAT solvingsuperposition calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (2)

SAT-Inspired Higher-Order Eliminations ⋮ A comprehensive framework for saturation theorem proving

Uses Software

• MiniSat
• OTTER
• VAMPIRE
• TPTP
• z3
• NiVER
• StarExec
• Bloqqer
• E Theorem Prover
• DISCOUNT
• ZRes
• AVATAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Labelled splitting
• Superposition with structural induction
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• On a generalization of extended resolution
• A combinator-based superposition calculus for higher-order logic
• SCL clause learning from simple models
• Faster, higher, stronger: E 2.3
• Revisiting enumerative instantiation
• Satisfiability modulo theories and assignments
• A unifying principle for clause elimination in first-order logic
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• AVATAR: The Architecture for First-Order Theorem Provers
• A Model-Constructing Satisfiability Calculus
• Efficient CNF Simplification Based on Binary Implication Graphs
• A Unified Proof System for QBF Preprocessing
• Congruence Closure with Free Variables
• Blocked Clause Elimination
• Efficient E-Matching for SMT Solvers
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Blocked Clauses in First-Order Logic
• SCAN—Elimination of predicate quantifiers
• Term Rewriting and All That
• Logics of Formal Inconsistency
• Clause Elimination Procedures for CNF Formulas
• The CADE-27 Automated theorem proving System Competition – CASC-27
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Blocked Clause Elimination for QBF
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Superposition with lambdas
• A comprehensive framework for saturation theorem proving

This page was built for publication: SAT-Inspired Eliminations for Superposition