The undecidability of the second order predicate unification problem

DOI10.1007/BF01621471MaRDI QIDQ2277244zbMATH OpenFDO

Authors Gilles Amiot

Publication date 1990

Published in Archive for Mathematical Logic (Search for Journal in Brave)

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

zbMATH Keywords

decidabilityfunction variablesone-place predicatesreductionunification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Review text

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.

Recommendations

• The undecidability of the second-order unification problem
• Simple second-order languages for which unification is undecidable
• On the undecidability of second-order unification
• The undecidability of the unification and matching problem for canonical theories
• Decidable higher-order unification problems

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 3923729 (Why is no real title available?)
• scientific article; zbMATH DE number 3590511 (Why is no real title available?)
• The undecidability of the second-order unification problem

Cited in

(12)

• The undecidability of the unification and matching problem for canonical theories
• The undecidability of the second-order unification problem
• The unification hierarchy is undecidable
• The subtyping problem for second-order types is undecidable.
• On the undecidability of second-order unification
• Tractable and intractable second-order matching problems
• Boolean unification with predicates
• The undecidability of the D_A-unification problem
• Bounded Second-Order Unification Is NP-Complete
• Existential type systems between Church and Curry style (type-free style)
• The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
• Simple second-order languages for which unification is undecidable

This page was built for publication: The undecidability of the second order predicate unification problem

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