Canonical Ground Horn Theories (Q4916071): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-37651-1_3
+Normal rank
@@ Property / OpenAlex ID @@
+W64666703
@@ Property / OpenAlex ID: W64666703 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385536
@@ Property / cites work: Q4385536 / rank @@
+Normal rank
@@ Property / cites work @@
+New results on rewrite-based satisfiability procedures
+Normal rank
@@ Property / cites work @@
+A rewriting approach to satisfiability procedures.
+Normal rank
@@ Property / cites work @@
+Equational inference, canonical proofs, and proof orderings
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Abstract congruence closure
@@ Property / cites work: Abstract congruence closure / rank @@
+Normal rank
@@ Property / cites work @@
+Theory reasoning in connection calculi
@@ Property / cites work: Theory reasoning in connection calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Q4667609
@@ Property / cites work: Q4667609 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5789040
@@ Property / cites work: Q5789040 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract canonical inference
@@ Property / cites work: Abstract canonical inference / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-Based Satisfiability Procedures for Recursive Data Structures
+Normal rank
@@ Property / cites work @@
+On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
+Normal rank
@@ Property / cites work @@
+Theory decision by decomposition
@@ Property / cites work: Theory decision by decomposition / rank @@
+Normal rank
@@ Property / cites work @@
+On rewrite programs: Semantics and relationship with prolog
+Normal rank
@@ Property / cites work @@
+Towards a foundation of completion procedures as semidecision procedures
+Normal rank
@@ Property / cites work @@
+On deciding satisfiability by theorem proving with speculative inferences
+Normal rank
@@ Property / cites work @@
+Completion Is an Instance of Abstract Canonical System Inference
+Normal rank
@@ Property / cites work @@
+Q2741274
@@ Property / cites work: Q2741274 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5679729
@@ Property / cites work: Q5679729 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4447230
@@ Property / cites work: Q4447230 / rank @@
+Normal rank
@@ Property / cites work @@
+A note on simplification orderings
@@ Property / cites work: A note on simplification orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Computing with rewrite systems
@@ Property / cites work: Computing with rewrite systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4036569
@@ Property / cites work: Q4036569 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012174
@@ Property / cites work: Q4012174 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract canonical presentations
@@ Property / cites work: Abstract canonical presentations / rank @@
+Normal rank
@@ Property / cites work @@
+Proving termination with multiset orderings
@@ Property / cites work: Proving termination with multiset orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Existence, Uniqueness, and Construction of Rewrite Systems
+Normal rank
@@ Property / cites work @@
+Q2751361
@@ Property / cites work: Q2751361 / rank @@
+Normal rank
@@ Property / cites work @@
+Deductive and inductive synthesis of equational programs
+Normal rank
@@ Property / cites work @@
+Q4447217
@@ Property / cites work: Q4447217 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear-time algorithms for testing the satisfiability of propositional horn formulae
+Normal rank
@@ Property / cites work @@
+Q2751377
@@ Property / cites work: Q2751377 / rank @@
+Normal rank
@@ Property / cites work @@
+An algorithm for finding canonical sets of ground rewrite rules in polynomial time
+Normal rank
@@ Property / cites work @@
+Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
+Normal rank
@@ Property / cites work @@
+A completion procedure for conditional equations
@@ Property / cites work: A completion procedure for conditional equations / rank @@
+Normal rank
@@ Property / cites work @@
+The integration of functions into logic programming: From theory to practice
+Normal rank
@@ Property / cites work @@
+On sentences which are true of direct unions of algebras
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving using term-rewriting systems
+Normal rank
@@ Property / cites work @@
+Rewrite method for theorem proving in first order theory with equality
+Normal rank
@@ Property / cites work @@
+Q3028369
@@ Property / cites work: Q3028369 / rank @@
+Normal rank
@@ Property / cites work @@
+A complete proof of correctness of the Knuth-Bendix completion algorithm
+Normal rank
@@ Property / cites work @@
+Simplifying conditional term rewriting systems: Unification, termination and confluence
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+On word problems in Horn theories
@@ Property / cites work: On word problems in Horn theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539637
@@ Property / cites work: Q4539637 / rank @@
+Normal rank
@@ Property / cites work @@
+Complexity and related enhancements for automated theorem-proving programs
+Normal rank
@@ Property / cites work @@
+The decision problem for some classes of sentences without quantifiers
+Normal rank
@@ Property / cites work @@
+Proof lengths for equational completion
@@ Property / cites work: Proof lengths for equational completion / rank @@
+Normal rank
@@ Property / cites work @@
+Q2859380
@@ Property / cites work: Q2859380 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction by theory resolution
@@ Property / cites work: Automated deduction by theory resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q4799892
@@ Property / cites work: Q4799892 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
+Normal rank
@@ Property / cites work @@
+A new method for the Boolean ring based theorem proving
+Normal rank
@@ Property / cites work @@
+Q4847001
@@ Property / cites work: Q4847001 / rank @@
+Normal rank