A unification algorithm for second-order monadic terms
From MaRDI portal
Publication:1109019
DOI10.1016/0168-0072(88)90015-2zbMath0655.03004OpenAlexW2074213277MaRDI QIDQ1109019
Publication date: 1988
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0168-0072(88)90015-2
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
Decidability of bounded second order unification ⋮ The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem ⋮ Simplifying the signature in second-order unification ⋮ Regular Patterns in Second-Order Unification ⋮ Some independence results for equational unification ⋮ The Kreisel length-of-proof problem ⋮ Tractable and intractable second-order matching problems ⋮ Equational unification, word unification, and 2nd-order equational unification ⋮ Unnamed Item ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ The undecidability of \(k\)-provability ⋮ Decidability of bounded higher-order unification ⋮ Completion of rewrite systems with membership constraints ⋮ Decidable higher-order unification problems ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Bounded arithmetic, proof complexity and two papers of Parikh ⋮ On the undecidability of second-order unification ⋮ Simple second-order languages for which unification is undecidable ⋮ \(\forall \exists^{5}\)-equational theory of context unification is undecidable
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The undecidability of the second-order unification problem
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- The Kreisel length-of-proof problem
- Equations in Free Groups
- Groups With Parametric Exponents
- An Efficient Unification Algorithm
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- Natural deduction as higher-order resolution
- A Machine-Oriented Logic Based on the Resolution Principle
- The undecidability of unification in third order logic
This page was built for publication: A unification algorithm for second-order monadic terms
