Linear second-order unification
From MaRDI portal
Publication:5055871
DOI10.1007/3-540-61464-8_63zbMath1503.68130OpenAlexW1501058900MaRDI QIDQ5055871
Publication date: 9 December 2022
Published in: Rewriting Techniques and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61464-8_63
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)
Related Items (12)
Decidability of bounded second order unification ⋮ Regular Patterns in Second-Order Unification ⋮ Dominance constraints in stratified context unification ⋮ Tractable and intractable second-order matching problems ⋮ Decidability of bounded higher-order unification ⋮ A decision algorithm for distributive unification ⋮ On equality up-to constraints over finite trees, context unification, and one-step rewriting ⋮ On the relation between context and sequence unification ⋮ Context unification with one context variable ⋮ On the undecidability of second-order unification ⋮ Solvability of context equations with two context variables is decidable ⋮ On rewrite constraints and context unification
Cites Work
- The undecidability of the second-order unification problem
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Bi-rewriting, a term rewriting technique for monotonic order relations
- A termination ordering for higher order rewrite systems
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- Makanin's algorithm for word equations-two improvements and a generalization
- Unnamed Item
- Unnamed Item
This page was built for publication: Linear second-order unification