scientific article
From MaRDI portal
Publication:3028369
zbMath0625.68068MaRDI QIDQ3028369
Michaël Rusinowitch, Jieh Hsiang
Publication date: 1987
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
theorem provingcompletenessconfluenceterm rewritinguniversal algebraequational theoriesword problemsKnuth-Bendix proceduresemi-decision proceduretransfinite semantic trees
Equational classes, universal algebra in model theory (03C05) Word problems (aspects of algebraic structures) (08A50)
Related Items
Semigroups satisfying x m+n = x n, A maximal-literal unit strategy for horn clauses, An application of automated equational reasoning to many-valued logic, Completion of first-order clauses with equality by strict superposition, Completion procedures as semidecision procedures, On subsumption in distributed derivations, Automated deduction with associative-commutative operators, On fairness of completion-based theorem proving strategies, Proving equational and inductive theorems by completion and embedding techniques, Improving transformation systems for general E-unification, Rewriting with a nondeterministic choice operator, Structures for abstract rewriting, Induction using term orders, Linear and unit-resulting refutations for Horn theories, Reasoning with conditional axioms, From diagrammatic confluence to modularity, The first-order theory of lexicographic path orderings is undecidable, A rewriting approach to satisfiability procedures., On using ground joinable equations in equational theorem proving, On the recursive decomposition ordering with lexicographical status and other related orderings, Automated proofs of the Moufang identities in alternative rings, Conditional equational theories and complete sets of transformations, A note on division orderings on strings, Fuzzy term-rewriting system, Towards a foundation of completion procedures as semidecision procedures, Using the tree representation of terms to recognize matching with neural networks, Learning domain knowledge to improve theorem proving, Canonical Ground Horn Theories, Hierarchical combination of intruder theories, Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures, Unification in Boolean rings and Abelian groups, Termination of rewrite systems by elementary interpretations, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Theorem-proving with resolution and superposition, On word problems in Horn theories, A completion procedure for conditional equations, Automatic proofs by induction in theories without constructors, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Automatic acquisition of search control knowledge from multiple proof attempts., Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, Single axioms for groups and abelian groups with various operations, The equational part of proofs by structural induction, Deductive and inductive synthesis of equational programs
