Linear second-order unification

DOI10.1007/3-540-61464-8_63zbMath1503.68130OpenAlexW1501058900MaRDI QIDQ5055871

Jordi Levy

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

Mathematics Subject Classification ID

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