A note on a canonical theory with undecidable unification and matching problem

DOI10.1007/BF00247435MaRDI QIDQ1098623zbMATH OpenOpenAlexFDO

Authors Alexander Bockmayr

Publication date 1987

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

Full work available at URL https://doi.org/10.1007/bf00247435

zbMATH Keywords

canonical term rewriting systemequational theoriesmatchingundecidabilityunification

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Abstract data types; algebraic specification (68Q65)

Review text

This research note gives a simple proof of the fact that the unification and matching problem is undecidable in the class of equational theories that can be embedded into a canonical term rewriting system. We present a canonical term rewriting system for integer arithmetic and show that the unification and matching problem in the corresponding equational theory is equivalent to Hilbert's tenth problem which is well known to be undecidable.

Recommendations

• The undecidability of the unification and matching problem for canonical theories
• On equational theories, unification, and (un)decidability
• The undecidability of the D_A-unification problem
• A remark on infinite matching vs infinite unification
• Unification in permutative equational theories is undecidable
• On unification: Equational theories are not bounded
• scientific article; zbMATH DE number 4041328
• The undecidability of the semi-unification problem
• Unification problem in equational theories
• On the undecidability of second-order unification

Cited in

(7)

• The undecidability of the unification and matching problem for canonical theories
• The undecidability of the semi-unification problem
• Unification in permutative equational theories is undecidable
• Rewriting, and equational unification: the higher-order cases
• A semantic approach to order-sorted rewriting
• Algebraic and logical aspects of unification
• Model-theoretic aspects of unification

This page was built for publication: A note on a canonical theory with undecidable unification and matching problem

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