scientific article
From MaRDI portal
zbMath0547.03012MaRDI QIDQ3338216
Publication date: 1984
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
diophantine equationterm structureequational theoriesassociative-commutative unificationtotal correctness of Stickel's algorithm
Free semigroups, generators and relations, word problems (20M05) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Diophantine equations (11D99)
Related Items
Mark Stickel: his earliest work, Alternating two-way AC-tree automata, Unification in combinations of collapse-free regular theories, An algebraic approach to unification under associativity and commutativity, History and basic features of the critical-pair/completion procedure, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Unification in commutative idempotent monoids, Finite generation of ambiguity in context-free languages, Combination of constraint solvers for free and quasi-free structures, Unification in commutative semigroups, Unification properties of commutative theories: A categorical treatment, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Nominal AC-matching, The calculus of context relations, Universal algebras, Bounded ACh unification, Completion for unification, Towards a foundation of completion procedures as semidecision procedures, Unification theory, AC-unification race: The system solving approach, implementation and benchmarks, Complexity of unification problems with associative-commutative operators, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, AC unification through order-sorted AC1 unification, Unification in commutative theories, Unification in a combination of arbitrary disjoint equational theories, Unnamed Item, Completion for rewriting modulo a congruence, Complete sets of unifiers and matchers in equational theories, Unification problem in equational theories, Unification algorithms cannot be combined in polynomial time., A superposition oriented theorem prover, Refutational theorem proving using term-rewriting systems
Uses Software
