Publication details

Saarland University Computer Science

A New Method for Undecidability Proofs of First Order Theories

Ralf Treinen

Journal of Symbolic Computation 14(5):437-457, November 1992

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 some interpretation. The goal of this paper is to define a framework for such reduction proofs. The method proposed is illustrated by proving the undecidability of the theory of a term algebra modulo the axioms of associativity and commutativity and of the theory of a partial lexicographic path ordering.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy