Simplifying the signature in second-order unification

DOI10.1007/s00200-009-0106-4zbMath1196.68113MaRDI QIDQ843951

Jordi Levy, Mateu Villaret

Publication date: 18 January 2010

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00200-009-0106-4

zbMATH Keywords

second-order unification; Currying; unification reduction

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

68Q42: Grammars and rewriting systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• 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
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Solvability of context equations with two context variables is decidable
• Higher order unification via explicit substitutions
• On the undecidability of second-order unification
• Decidability of bounded second order unification
• Solving equations with sequence variables and sequence functions
• Satisfiability of word equations with constants is in NEXPTIME
• Satisfiability of equations in free groups is in PSPACE
• Bounded Second-Order Unification Is NP-Complete
• Stratified Context Unification Is NP-Complete
• Decidability of the unification problem for second-order languages with unary functional symbols
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• A Decision Algorithm for Stratified Context Unification
• Explicit substitutions
• Automated Deduction – CADE-20
• Sequence Unification Through Currying
• Database Programming Languages
• Rewriting Techniques and Applications
• Rewriting Techniques and Applications