SAT-Inspired Eliminations for Superposition (Q5875949): Difference between revisions

@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AVATAR
@@ Property / describes a project that uses: AVATAR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1145/3565366
@@ Property / full work available at URL: https://doi.org/10.1145/3565366 / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W4298140626
@@ Property / OpenAlex ID: W4298140626 / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Congruence Closure with Free Variables
@@ Property / cites work: Congruence Closure with Free Variables / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with lambdas
@@ Property / cites work: Superposition with lambdas / rank @@
+Normal rank
@@ Property / cites work @@
+A combinator-based superposition calculus for higher-order logic
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Blocked Clause Elimination for QBF
@@ Property / cites work: Blocked Clause Elimination for QBF / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability modulo theories and assignments
@@ Property / cites work: Satisfiability modulo theories and assignments / rank @@
+Normal rank
@@ Property / cites work @@
+On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
+Normal rank
@@ Property / cites work @@
+Logics of Formal Inconsistency
@@ Property / cites work: Logics of Formal Inconsistency / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723442
@@ Property / cites work: Q2723442 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with structural induction
@@ Property / cites work: Superposition with structural induction / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+A Model-Constructing Satisfiability Calculus
@@ Property / cites work: A Model-Constructing Satisfiability Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Labelled splitting
@@ Property / cites work: Labelled splitting / rank @@
+Normal rank
@@ Property / cites work @@
+SCL clause learning from simple models
@@ Property / cites work: SCL clause learning from simple models / rank @@
+Normal rank
@@ Property / cites work @@
+Q4863622
@@ Property / cites work: Q4863622 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3743300
@@ Property / cites work: Q3743300 / rank @@
+Normal rank
@@ Property / cites work @@
+A Unified Proof System for QBF Preprocessing
@@ Property / cites work: A Unified Proof System for QBF Preprocessing / rank @@
+Normal rank
@@ Property / cites work @@
+Clause Elimination Procedures for CNF Formulas
@@ Property / cites work: Clause Elimination Procedures for CNF Formulas / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient CNF Simplification Based on Binary Implication Graphs
+Normal rank
@@ Property / cites work @@
+Blocked Clause Elimination
@@ Property / cites work: Blocked Clause Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Predicate Elimination for Preprocessing in First-Order Theorem Proving
+Normal rank
@@ Property / cites work @@
+A unifying principle for clause elimination in first-order logic
+Normal rank
@@ Property / cites work @@
+Blocked Clauses in First-Order Logic
@@ Property / cites work: Blocked Clauses in First-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+On a generalization of extended resolution
@@ Property / cites work: On a generalization of extended resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751358
@@ Property / cites work: Q2751358 / rank @@
+Normal rank
@@ Property / cites work @@
+SCAN—Elimination of predicate quantifiers
@@ Property / cites work: SCAN—Elimination of predicate quantifiers / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751378
@@ Property / cites work: Q2751378 / rank @@
+Normal rank
@@ Property / cites work @@
+Revisiting enumerative instantiation
@@ Property / cites work: Revisiting enumerative instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Faster, higher, stronger: E 2.3
@@ Property / cites work: Faster, higher, stronger: E 2.3 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
+Normal rank
@@ Property / cites work @@
+The CADE-27 Automated theorem proving System Competition – CASC-27
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank
@@ Property / cites work @@
+A comprehensive framework for saturation theorem proving
+Normal rank
@@ Property / Wikidata QID @@
+Q130866229
@@ Property / Wikidata QID: Q130866229 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5875949