Simple second-order languages for which unification is undecidable

DOI10.1016/S0304-3975(06)80003-4MaRDI QIDQ807609zbMATH OpenFDO

Authors William M. Farmer

Publication date 1991

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(06)80003-4

zbMATH Keywords

second-order unificationundecidability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Review text

Second-order substitutions are applied to terms constructed from individual and function constants and variables. Such a substitution \(\sigma\) assigns terms to individual variables and \(\lambda\)-expressions of the form \(\lambda x_ 1...\lambda x_ n t\) to n-place function variables. \(\sigma\) unifies terms s, u if \(s\sigma\) and \(u\sigma\) are equal after \(\lambda\)-conversion is performed. The author proved earlier [Ann. Pure Appl. Logic 39, No.2, 131-174 (1988; Zbl 0655.03004)] that the second-order unification problem is decidable when all function constants are monadic. Goldfarb proved that there is a language for which the second-order unification problem is undecidable. In the paper under review the author proves that for certain n this problem is undecidable for any language which has a nonmonadic constant and at least n function variables.

Recommendations

• The undecidability of the second-order unification problem
• On the undecidability of second-order unification
• A unification algorithm for second-order monadic terms
• The undecidability of the second order predicate unification problem
• Simplifying the signature in second-order unification

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A unification algorithm for second-order monadic terms
• A unification-theoretic method for investigating the \(k\)-provability problem
• An Efficient Unification Algorithm
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Hilbert's Tenth Problem is Unsolvable
• scientific article; zbMATH DE number 3878393 (Why is no real title available?)
• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• Linear unification
• Natural deduction as higher-order resolution
• Proving and applying program transformations expressed with second-order patterns
• Some Results on the Length of Proofs
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic

Cited in

(17)

• The undecidability of the second-order unification problem
• The Kreisel length-of-proof problem
• Farmer's theorem revisited
• \(\forall \exists^{5}\)-equational theory of context unification is undecidable
• A unification-theoretic method for investigating the \(k\)-provability problem
• Higher-order unification revisited: Complete sets of transformations
• On the undecidability of second-order unification
• The undecidability of the second order predicate unification problem
• Referential logic of proofs
• Tractable and intractable second-order matching problems
• Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent
• Expressing symmetry breaking in DRAT proofs
• scientific article; zbMATH DE number 2090082 (Why is no real title available?)
• An algorithm for distributive unification
• Decidable higher-order unification problems
• RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION
• Simplifying the signature in second-order unification

This page was built for publication: Simple second-order languages for which unification is undecidable

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