E-unification with constants vs. general E-unification

DOI10.1007/S10817-010-9201-2MaRDI QIDQ438584zbMATH OpenOpenAlexFDO

Authors Jan Otop

Publication date 31 July 2012

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9201-2

zbMATH Keywords

\(E\)-unification with constantscombination problemgeneral \(E\)-unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• Some results on equational unification
• scientific article; zbMATH DE number 4080961
• A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms
• Combination techniques and decision problems for disunification
• Combination techniques and decision problems for disunification

Cites work

• Complexity of unification problems with associative-commutative operators
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• Single versus simultaneous equational unification and equational unification for variable-permuting theories
• Term Rewriting and All That
• Unification in a combination of arbitrary disjoint equational theories
• Unification in commutative idempotent monoids
• Unification in the union of disjoint equational theories: Combining decision procedures
• Unification theory

Cited in

(1)

• Model measuring for discrete and hybrid systems

This page was built for publication: \(E\)-unification with constants vs. general \(E\)-unification

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