scientific article; zbMATH DE number 4049130

zbMATH Open0643.68137MaRDI QIDQ3786019FDOQ3786019

Authors: Alexander Herold 

Publication date: 1986

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 4112560
• Combining unification algorithms
• Unification in the union of disjoint equational theories: Combining decision procedures
• Unification in a combination of equational theories: an efficient algorithm
• Unification in combinations of collapse-free regular theories

zbMATH Keywords

automated deductionequational theoriesunification algorithmscomplete set of unifiersdisjoint function symbols

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Mechanization of proofs and logical operations (03B35)

Cited In (32)

• Title not available (Why is that?)
• Unification algorithms cannot be combined in polynomial time.
• On equational theories, unification, and (un)decidability
• Unification theory
• Unification algorithms cannot be combined in polynomial time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Matching - a special case of unification?
• Title not available (Why is that?)
• Unification Modulo Builtins
• Unification in a combination of arbitrary disjoint equational theories
• Associative-commutative unification
• Unification in combinations of collapse-free regular theories
• Combining matching algorithms: The regular case
• Title not available (Why is that?)
• Unification in Boolean rings
• A practical unification algorithm
• Combining matching algorithms: The regular case
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Boolean unification - the story so far
• Set unification
• Automata-driven efficient subterm unification
• Model-theoretic aspects of unification
• Modular higher-order E-unification
• Title not available (Why is that?)
• Combining unification algorithms
• Second-order unification in the presence of linear shallow algebraic equations
• Unification problem in equational theories
• Combining equational reasoning
• A new approach to general E-unification based on conditional rewriting systems

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3786019)