Simple second-order languages for which unification is undecidable
From MaRDI portal
Publication:807609
DOI10.1016/S0304-3975(06)80003-4zbMath0731.03005MaRDI QIDQ807609
Publication date: 1991
Published in: Theoretical Computer Science (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Simplifying the signature in second-order unification ⋮ Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent ⋮ Expressing Symmetry Breaking in DRAT Proofs ⋮ An algorithm for distributive unification ⋮ The Kreisel length-of-proof problem ⋮ Tractable and intractable second-order matching problems ⋮ Referential logic of proofs ⋮ Decidable higher-order unification problems ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION ⋮ On the undecidability of second-order unification ⋮ Farmer's theorem revisited ⋮ \(\forall \exists^{5}\)-equational theory of context unification is undecidable
Cites Work
- Unnamed Item
- Unnamed Item
- A unification algorithm for second-order monadic terms
- The undecidability of the second-order unification problem
- Linear unification
- Proving and applying program transformations expressed with second-order patterns
- A unification-theoretic method for investigating the \(k\)-provability problem
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- An Efficient Unification Algorithm
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- Hilbert's Tenth Problem is Unsolvable
- Natural deduction as higher-order resolution
- A Machine-Oriented Logic Based on the Resolution Principle
- The undecidability of unification in third order logic
- Some Results on the Length of Proofs
This page was built for publication: Simple second-order languages for which unification is undecidable
