scientific article
From MaRDI portal
Publication:3786019
zbMath0643.68137MaRDI QIDQ3786019
Publication date: 1986
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
automated deductionequational theoriesunification algorithmscomplete set of unifiersdisjoint function symbols
Mechanization of proofs and logical operations (03B35) General topics in the theory of software (68N01)
Related Items (16)
A new approach to general E-unification based on conditional rewriting systems ⋮ Second-order unification in the presence of linear shallow algebraic equations ⋮ Modular higher-order E-unification ⋮ Associative-commutative unification ⋮ Unification in Boolean rings ⋮ Combining matching algorithms: The regular case ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Unification theory ⋮ Combining matching algorithms: The regular case ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Matching - a special case of unification? ⋮ Boolean unification - the story so far ⋮ Unification problem in equational theories ⋮ On equational theories, unification, and (un)decidability ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Unification algorithms cannot be combined in polynomial time.
This page was built for publication: