Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231): Difference between revisions

@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Semantically-guided goal-sensitive reasoning: inference system and completeness
+Normal rank
@@ Property / cites work @@
+Q5679729
@@ Property / cites work: Q5679729 / rank @@
+Normal rank
@@ Property / cites work @@
+Stratified resolution
@@ Property / cites work: Stratified resolution / rank @@
+Normal rank
@@ Property / cites work @@
+On finding short resolution refutations and small unsatisfiable subsets
+Normal rank
@@ Property / cites work @@
+Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
+Normal rank
@@ Property / cites work @@
+Q3618853
@@ Property / cites work: Q3618853 / rank @@
+Normal rank
@@ Property / cites work @@
+Another Generalization of Resolution
@@ Property / cites work: Another Generalization of Resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Clause Elimination for SAT and QSAT
@@ Property / cites work: Clause Elimination for SAT and QSAT / rank @@
+Normal rank
@@ Property / cites work @@
+Selecting the Selection
@@ Property / cites work: Selecting the Selection / rank @@
+Normal rank
@@ Property / cites work @@
+The 481 Ways to Split a Clause and Deal with Propositional Variables
+Normal rank
@@ Property / cites work @@
+Scavenger 0.1: a theorem prover based on conflict resolution
+Normal rank
@@ Property / cites work @@
+Blocked Clause Elimination
@@ Property / cites work: Blocked Clause Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E.T. 0.1
@@ Property / cites work: System Description: E.T. 0.1 / rank @@
+Normal rank
@@ Property / cites work @@
+Super-Blocked Clauses
@@ Property / cites work: Super-Blocked Clauses / rank @@
+Normal rank
@@ Property / cites work @@
+A unifying principle for clause elimination in first-order logic
+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 @@
+Complexity and related enhancements for automated theorem-proving programs
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+A simplified way of proving trade-off results for resolution
+Normal rank
@@ Property / cites work @@
+History and Prospects for First-Order Automated Deduction
+Normal rank
@@ Property / cites work @@
+The search efficiency of theorem proving strategies
+Normal rank
@@ Property / cites work @@
+Limited resource strategy in resolution theorem proving
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Q5541351
@@ Property / cites work: Q5541351 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2724150
@@ Property / cites work: Q2724150 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4797437
@@ Property / cites work: Q4797437 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / rank @@
+Normal rank
@@ Property / cites work @@
+Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
+Normal rank
@@ Property / cites work @@
+Detecting inconsistencies in large first-order knowledge bases
+Normal rank
@@ Property / cites work @@
+Abstract interpretation as automated deduction
@@ Property / cites work: Abstract interpretation as automated deduction / rank @@
+Normal rank
@@ Property / cites work @@
+Schubert's steamroller problem: Formulations and solutions
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+Q4585854
@@ Property / cites work: Q4585854 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
+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 / OpenAlex ID @@
+W2808325100
@@ Property / OpenAlex ID: W2808325100 / rank @@
+Normal rank