Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732): Difference between revisions

@@ Property / describes a project that uses @@
+OTTER
@@ Property / describes a project that uses: OTTER / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SETHEO
@@ Property / describes a project that uses: SETHEO / 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 @@
+METEOR
@@ Property / describes a project that uses: METEOR / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Refutations by Matings
@@ Property / cites work: Refutations by Matings / rank @@
+Normal rank
@@ Property / cites work @@
+The use of lemmas in the model elimination procedure
+Normal rank
@@ Property / cites work @@
+Short proofs of the pigeonhole formulas based on the connection method
+Normal rank
@@ Property / cites work @@
+Q5679729
@@ Property / cites work: Q5679729 / rank @@
+Normal rank
@@ Property / cites work @@
+Many hard examples for resolution
@@ Property / cites work: Many hard examples for resolution / rank @@
+Normal rank
@@ Property / cites work @@
+The relative efficiency of propositional proof systems
+Normal rank
@@ Property / cites work @@
+The intractability of resolution
@@ Property / cites work: The intractability of resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q5572939
@@ Property / cites work: Q5572939 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear resolution with selection function
@@ Property / cites work: Linear resolution with selection function / rank @@
+Normal rank
@@ Property / cites work @@
+Controlled integration of the cut rule into connection tableau calculi
+Normal rank
@@ Property / cites work @@
+SETHEO: A high-performance theorem prover
@@ Property / cites work: SETHEO: A high-performance theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical Theorem-Proving by Model Elimination
@@ Property / cites work: Mechanical Theorem-Proving by Model Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+An extension to linear resolution with selection function
+Normal rank
@@ Property / cites work @@
+Dissolution
@@ Property / cites work: Dissolution / rank @@
+Normal rank
@@ Property / cites work @@
+Two Results on Ordering for Resolution with Merging and Linear Format
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Refutation graphs
@@ Property / cites work: Refutation graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Avoiding duplicate proofs with the foothold refinement
+Normal rank
@@ Property / cites work @@
+A Prolog technology theorem prover: Implementation by an extended Prolog compiler
+Normal rank
@@ Property / cites work @@
+A Prolog technology theorem prover: A new exposition and implementation in Prolog
+Normal rank
@@ Property / cites work @@
+Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
+Normal rank
@@ Property / cites work @@
+The TPTP problem library
@@ Property / cites work: The TPTP problem library / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994754
@@ Property / cites work: Q3994754 / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/s0004-3702(96)00046-x
+Normal rank
@@ Property / OpenAlex ID @@
+W1970444992
@@ Property / OpenAlex ID: W1970444992 / rank @@
+Normal rank