The following pages link to (Q3028369):
Displaying 44 items.
- Unification in Boolean rings and Abelian groups (Q582073) (← links)
- Towards a foundation of completion procedures as semidecision procedures (Q673134) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- On word problems in Horn theories (Q757095) (← links)
- A completion procedure for conditional equations (Q758211) (← links)
- On the recursive decomposition ordering with lexicographical status and other related orderings (Q912609) (← links)
- Automated proofs of the Moufang identities in alternative rings (Q912653) (← links)
- Conditional equational theories and complete sets of transformations (Q918541) (← links)
- A note on division orderings on strings (Q918714) (← links)
- Rewriting with a nondeterministic choice operator (Q1096383) (← links)
- Fuzzy term-rewriting system (Q1182011) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- Single axioms for groups and abelian groups with various operations (Q1312155) (← links)
- The equational part of proofs by structural induction (Q1317862) (← links)
- Deductive and inductive synthesis of equational programs (Q1322836) (← links)
- On subsumption in distributed derivations (Q1337562) (← links)
- Automated deduction with associative-commutative operators (Q1340508) (← links)
- The first-order theory of lexicographic path orderings is undecidable (Q1392274) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- On using ground joinable equations in equational theorem proving (Q1404987) (← links)
- Termination of rewrite systems by elementary interpretations (Q1805401) (← links)
- Automatic proofs by induction in theories without constructors (Q1824382) (← links)
- Automatic acquisition of search control knowledge from multiple proof attempts. (Q1854367) (← links)
- Induction using term orders (Q1915132) (← links)
- Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
- Reasoning with conditional axioms (Q1924731) (← links)
- From diagrammatic confluence to modularity (Q1929228) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures (Q2268100) (← links)
- Hierarchical combination of intruder theories (Q2482450) (← links)
- Structures for abstract rewriting (Q2642463) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Using the tree representation of terms to recognize matching with neural networks (Q4375956) (← links)
- Learning domain knowledge to improve theorem proving (Q4647500) (← links)
- Canonical Ground Horn Theories (Q4916071) (← links)
- On fairness of completion-based theorem proving strategies (Q5055773) (← links)
- Proving equational and inductive theorems by completion and embedding techniques (Q5055774) (← links)
- Improving transformation systems for general E-unification (Q5055788) (← links)
- Semigroups satisfying x m+n = x n (Q5881194) (← links)
- A maximal-literal unit strategy for horn clauses (Q5881264) (← links)
- An application of automated equational reasoning to many-valued logic (Q5881275) (← links)
- Completion of first-order clauses with equality by strict superposition (Q5881276) (← links)
- Completion procedures as semidecision procedures (Q5881279) (← links)
