Abstract
A natural example of a canonical theory with undecidable unification and matching problem is presented.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Davis, M. (1973) ‘Hilbert's tenth problem is unsolvable’, Amer. Math. Monthly 80 233–269.
Göbel, R. (1986) Private Communication, University of Kaiserslautern, Fachbereich Informatik, Postfach 3049, D-6750 Kaiserslautern, F.R.G.
Heilbrunner, S. and Hölldobler, S. (1986) ‘The undecidability of the unification and matching problem for canonical theories’, submitted to Acta Informatica.
Huet, G. and Oppen, D. C. (1980) ‘Equations and rewrite rules: A survey’, in Formal Languages: Perspectives and Open Problems, Book, R. (ed.), Academic Press, pp. 349–405.
Matijasevich, Y. (1970) ‘Enumerable sets are diophantine’, Sov. Math. Doklady 11 354–357.
Réty, P., Kirchner, C., Kirchner, H., and Lescanne, P. (1985) NARROWER: A new Algorithm for Unification and its Applications to Logic Programming, Rewriting Techniques and Applications, Dijon Springer LNCS 202, pp. 141–155.
Siekmann, J. (1986) Unification Theory. Proc. of 8th ECAI-86, Brighton, pp. vi–xxxv
Szabo, P. (1982) ‘Unifikationstheorie Erster Ordnung’, Dissertation (in German), Universität Karlsruhe.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Bockmayr, A. A note on a canonical theory with undecidable unification and matching problem. J Autom Reasoning 3, 379–381 (1987). https://doi.org/10.1007/BF00247435
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00247435