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)

zbMATH Keywords

undecidabilitysecond-order unification

Mathematics Subject Classification ID

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

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

• scientific article; zbMATH DE number 3878393 (Why is no real title available?)
• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• 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
• 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

(16)

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

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)