Simple second-order languages for which unification is undecidable

DOI10.1016/S0304-3975(06)80003-4zbMATH Open0731.03005MaRDI QIDQ807609FDOQ807609

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)

Cites Work

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

Cited In (15)

• Farmer's theorem revisited
• \(\forall \exists^{5}\)-equational theory of context unification is undecidable
• Simplifying the signature in second-order unification
• Higher-order unification revisited: Complete sets of transformations
• Referential logic of proofs
• Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
• On the undecidability of second-order unification
• Tractable and intractable second-order matching problems
• An algorithm for distributive unification
• Title not available (Why is that?)
• Expressing Symmetry Breaking in DRAT Proofs
• Decidable higher-order unification problems
• RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION
• A unification-theoretic method for investigating the \(k\)-provability problem
• The Kreisel length-of-proof problem

   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 👍 👎

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)