On the undecidability of second-order unification
From MaRDI portal
Publication:1854349
DOI10.1006/inco.2000.2877zbMath1005.03007OpenAlexW2150481709MaRDI QIDQ1854349
Publication date: 14 January 2003
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.2000.2877
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Decidability of bounded second order unification ⋮ Simplifying the signature in second-order unification ⋮ Tractable and intractable second-order matching problems ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ Nominal syntax with atom substitutions ⋮ In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming ⋮ Decidability of bounded higher-order unification ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types ⋮ Nominal Unification from a Higher-Order Perspective ⋮ The Existential Fragment of the One-Step Parallel Rewriting Theory ⋮ Solvability of context equations with two context variables is decidable ⋮ Farmer's theorem revisited ⋮ \(\forall \exists^{5}\)-equational theory of context unification is undecidable
Cites Work
- The undecidability of simultaneous rigid E-unification
- Simple second-order languages for which unification is undecidable
- A unification algorithm for second-order monadic terms
- The undecidability of the second-order unification problem
- Proving and applying program transformations expressed with second-order patterns
- Third order matching is decidable
- Logic with equality: Partisan corroboration and shifted pairing
- Decidability of the unification problem for second-order languages with unary functional symbols
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- Monadic simultaneous rigid E-unification and related problems
- Linear second-order unification
- Decidable higher-order unification problems
- On equality up-to constraints over finite trees, context unification, and one-step rewriting
- Tree generating regular systems
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: On the undecidability of second-order unification
