SCL(EQ): SCL for first-order logic with equality (Q2104511): Difference between revisions

@@ Property / describes a project that uses @@
+iProver-Eq
@@ Property / describes a project that uses: iProver-Eq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Darwin
@@ Property / describes a project that uses: Darwin / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+iProver
@@ Property / describes a project that uses: iProver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E-Darvin
@@ Property / describes a project that uses: E-Darvin / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W4289104055
@@ Property / OpenAlex ID: W4289104055 / rank @@
+Normal rank
@@ Property / cites work @@
+NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q4249897
@@ Property / cites work: Q4249897 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4282593
@@ Property / cites work: Q4282593 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3838803
@@ Property / cites work: Q3838803 / rank @@
+Normal rank
@@ Property / cites work @@
+Lemma Learning in the Model Evolution Calculus
@@ Property / cites work: Lemma Learning in the Model Evolution Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Hyper Tableaux with Equality
@@ Property / cites work: Hyper Tableaux with Equality / rank @@
+Normal rank
@@ Property / cites work @@
+Model evolution with equality -- revised and implemented
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition and Model Evolution Combined
@@ Property / cites work: Superposition and Model Evolution Combined / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+On First-Order Model-Based Reasoning
@@ Property / cites work: On First-Order Model-Based Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / 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 @@
+Q2751361
@@ Property / cites work: Q2751361 / 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 @@
+Subsumption demodulation in first-order theorem proving
+Normal rank
@@ Property / cites work @@
+Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
+Normal rank
@@ Property / cites work @@
+Labelled Unit Superposition Calculi for Instantiation-Based Reasoning
+Normal rank
@@ Property / cites work @@
+Fast Decision Procedures Based on Congruence Closure
+Normal rank
@@ Property / cites work @@
+Ordered semantic hyper-linking
@@ Property / cites work: Ordered semantic hyper-linking / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624683
@@ Property / cites work: Q5624683 / 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 @@
+A comprehensive framework for saturation theorem proving
+Normal rank
@@ Property / cites work @@
+Q2751379
@@ Property / cites work: Q2751379 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning Building Blocks
@@ Property / cites work: Automated Reasoning Building Blocks / rank @@
+Normal rank
@@ Property / cites work @@
+Subterm contextual rewriting
@@ Property / cites work: Subterm contextual rewriting / rank @@
+Normal rank