Abstract
We claim that the reduction of Post's Correspondence Problem to the decision problem of a theory provides a useful tool for proving undecidability of first order theories given by an interpretation. The goal of this paper is to propose a framework for such reduction proofs. The method proposed is illustrated by proving the undecidability of the theory of a term algebra modulo AC and the theory of a partial lexicographic path ordering.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Hans-Jürgen Bürckert, Alexander Herold, and Manfred Schmidt-Schauß. On Equational Theories, Unification and Decidability. SEKI-Report SR-86-20, Universität Kaiserslautern, 1986.
Hans-Jürgen Bürckert and Manfred Schmidt-Schauß. On the Solvability of Equational Problems. SEKI Report SR-89-07, Universität Kaiserslautern, 1989.
Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7(3,4):371–425, 1989.
Hubert Comon. Unification et Disunification. Théorie et Applications. PhD thesis, Institut National Polytechnique de Grenoble, Grenoble, France, 1988.
Hubert Comon. Disunification:A Survey. Rapport de Recherche no. 540, LRI, Université de Pairs Sud, january 1990.
Hubert Comon. Solving inequations in term algebras. In 5th Symposium on Logic in Computer Science, 1990.
Martin Davis. Unsolvable problems. In Jon Barwise, editor, Handbook of Mathematical Logic, chapter C.2, pages 567–594, North-Holland, 1977.
Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 7:279–301, 1982.
Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification, vol. 1. EATCS-Monographs on Theoretical Computer Science, Springer-Verlag, 1985.
Herbert B. Enderton. Mathematical Introduction to Logic. Academic Press, 1972.
Jean H. Gallier. Logic for Computer Science. Harper & Row, publishers, 1986.
Kurt Gödel. Über Formal Unentscheidbare Sätze der Pricipia Mathematica und Verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931.
H. Jerome Keisler. Model Theory for Infinitary Logic. Studies in Logic and the Foundations of Mathematics, vol. 62, North-Holland Publishing Company, 1971.
Claude Kirchner. Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories %Equationelles. PhD thesis, Centre de R%echerche en Informatique de Nancy, 1985.
Yu Matijacevič. Enumerable sets are diophantine. Dokl. Akad. Nauk. SSSR, 191:279–282, 1970.
G. D. Plotkin. Building-in equational theories. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, pages 73–90, Edinburgh University Press, 1972.
Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the AMS, 52:264–268, 1946.
W. V. Quine. Concatenation as a basis for arithmetic. Journal of Symbolic Logic, 11(4):105–114, 1946.
M. O. Rabin. A simple method for undecidability proofs and some applications. In Yehoshua Bar-Hillel, editor, Logic, Methodology and Philosophy of Science, pages 58–68, North-Holland, 1965.
Hartley Rogers, Jr. Theory of Recursive Functions and Effective Computability. MIT Press, second edition, 1987.
Jörg H. Siekmann. Unification theory. A survey. Journal of Symbolic Logic, 1989.
Mark E. Stickel. A unification algorithm for associative-commutative functions. Journal of the ACM, 28(3):423–434, 1981.
Alfred Tarski. A general method in proofs of undecidability. In Alfred Tarski, Andrzej Mostowski, and Raphael M. Robinson, editors, Undecidable Theories, pages 1–35, North-Holland, 1953.
Ralf Treinen. A new method for undecidability proof of first order theories. Technical Report A 09/90, Universität des Saarlandes, Saarbrücken, may 1990.
K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebra. Journal of the ACM, 34(2):492–510, april 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Treinen, R. (1990). A new method for undecidability proofs of first order theories. In: Nori, K.V., Veni Madhavan, C.E. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1990. Lecture Notes in Computer Science, vol 472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53487-3_34
Download citation
DOI: https://doi.org/10.1007/3-540-53487-3_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53487-7
Online ISBN: 978-3-540-46313-9
eBook Packages: Springer Book Archive