Decidability of bounded second order unification

DOI10.1016/j.ic.2003.08.002zbMath1078.68139OpenAlexW2096032711MaRDI QIDQ1887168

Manfred Schmidt-Schauss

Publication date: 23 November 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: http://publikationen.ub.uni-frankfurt.de/files/4584/bouncsl.pdf

zbMATH Keywords

Automated deductionLambda calculusUnificationRewritingContext unificationHigher-order unificationLogics in artificial intelligenceSecond-order unification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Simplifying the signature in second-order unification ⋮ On the building of affine retractions ⋮ Decidability of bounded higher-order unification ⋮ On rewrite constraints and context unification

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Completion of rewrite systems with membership constraints. II: Constraint solving
• A decision algorithm for distributive unification
• Solvability of context equations with two context variables is decidable
• Higher-order unification revisited: Complete sets of transformations
• On the undecidability of second-order unification
• Satisfiability of word equations with constants is in NEXPTIME
• Proving termination with multiset orderings
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• A Decision Algorithm for Stratified Context Unification
• Linear second-order unification