The undecidability of the second order predicate unification problem (Q2277244)

In diesem Artikel betrachtet der Verf. zwei Sprachen: \(L_ t\)- die Sprache von Termen, die Individuenvariable, einstellige Funktionenvariable und Konstanten enthalten -, und \(L_ p\)- die Sprache atomarer Formeln, die Individuenvariable, einstellige Prädikatvariable und Konstanten enthalten. Das Unifikationsproblem ist das Problem, für eine endliche Menge von Termen bzw. Formeln \(\{<t_ i,u_ i>:\) \(1\leq i\leq n\}\) eine Substitution \(\sigma\) zu finden, so daß für jedes i, \(\sigma t_ i=\sigma u_ i\) gilt. Es wird bewiesen, daß es für jede solche Menge in \(L_ t\) eine Menge in \(L_ p\) gibt, deren Unifikationsmöglichkeit mit der von der ersten Menge gleichwertig ist. Weil das Unifikationsproblem in \(L_ t\) unentscheidbar ist, wenn die Sprache eine Funktionenkonstante mit Stellenzahl \(\geq 2\) enthält, folgt aus dem bewiesenen Resultat, daß das Unifikationsproblem für \(L_ p\) unter derselben Bedingung unentscheidbar ist.