scientific article; zbMATH DE number 4112560

MaRDI QIDQ3835440zbMATH OpenFDO

Authors Alexander Herold

Publication date 1987

zbMATH Keywords

equational theoriesunification algorithms

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05)

Recommendations

• Unification in combinations of collapse-free regular theories
• scientific article; zbMATH DE number 4049130
• Combining unification algorithms
• Unification in a combination of arbitrary disjoint equational theories
• Unification in a combination of equational theories: an efficient algorithm

Cited in

(37)

• Unification in combinations of collapse-free regular theories
• Combining matching algorithms: The regular case
• AC-unification race: The system solving approach, implementation and benchmarks
• Competing for the \(AC\)-unification race
• Completeness results for basic narrowing
• Combining unification algorithms
• Single versus simultaneous equational unification and equational unification for variable-permuting theories
• On equational theories, unification, and (un)decidability
• Unification in the union of disjoint equational theories: Combining decision procedures
• Rule-based unification in combined theories and the finite variant property
• Restricted combinatory unification
• Unification modulo an equality theory for equational logic programming
• Unification and combination of a class of traversal strategies made with pattern matching and fixed-points
• scientific article; zbMATH DE number 1722699 (Why is no real title available?)
• scientific article; zbMATH DE number 3866609 (Why is no real title available?)
• scientific article; zbMATH DE number 3871334 (Why is no real title available?)
• scientific article; zbMATH DE number 3945372 (Why is no real title available?)
• scientific article; zbMATH DE number 4049130 (Why is no real title available?)
• scientific article; zbMATH DE number 4092822 (Why is no real title available?)
• Formal synthesis of a unification algorithm by the deductive-tableau method
• scientific article; zbMATH DE number 36613 (Why is no real title available?)
• scientific article; zbMATH DE number 176128 (Why is no real title available?)
• scientific article; zbMATH DE number 1552528 (Why is no real title available?)
• A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms
• Unification algorithms cannot be combined in polynomial time
• Verification of the Completeness of Unification Algorithms à la Robinson
• Combining matching algorithms: The regular case
• Decidability of confluence and termination of monadic term rewriting systems
• Unification properties of commutative theories: a categorical treatment
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Term Rewriting and Applications
• Unification in commutative theories
• Unification in a combination of arbitrary disjoint equational theories
• A new approach to general E-unification based on conditional rewriting systems
• Unification in varieties of completely regular semigroups
• Unification theory
• Unification in a combination of equational theories: an efficient algorithm

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 Q3835440)