Decidability of bounded second order unification

DOI10.1016/J.IC.2003.08.002MaRDI QIDQ1887168zbMATH OpenOpenAlexFDO

Authors Manfred Schmidt-Schauß

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

UnificationLambda calculusAutomated deductionRewritingContext unificationHigher-order unificationLogics in artificial intelligenceSecond-order unification

Mathematics Subject Classification ID

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

Recommendations

• On the complexity of bounded second-order unification and stratified context unification
• Bounded Second-Order Unification Is NP-Complete
• On the undecidability of second-order unification
• Decidable higher-order unification problems
• scientific article; zbMATH DE number 1948184

Cites work

• scientific article; zbMATH DE number 1189058 (Why is no real title available?)
• scientific article; zbMATH DE number 1189059 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1341608 (Why is no real title available?)
• scientific article; zbMATH DE number 592368 (Why is no real title available?)
• scientific article; zbMATH DE number 1161563 (Why is no real title available?)
• A Decision Algorithm for Stratified Context Unification
• A decision algorithm for distributive unification
• A unification algorithm for second-order monadic terms
• 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
• Higher-order unification revisited: Complete sets of transformations
• Linear second-order unification
• On the undecidability of second-order unification
• Proving termination with multiset orderings
• Satisfiability of word equations with constants is in NEXPTIME
• Solvability of context equations with two context variables is decidable
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The undecidability of the second-order unification problem

Cited in

(12)

• Improved witnessing and local improvement principles for second-order bounded arithmetic
• On the building of affine retractions
• How to prove decidability of equational theories with second-order computation analyser SOL
• scientific article; zbMATH DE number 1189058 (Why is no real title available?)
• On the complexity of bounded second-order unification and stratified context unification
• scientific article; zbMATH DE number 1948184 (Why is no real title available?)
• On rewrite constraints and context unification
• Linear second-order unification
• Decidability of bounded higher-order unification
• Bounded Second-Order Unification Is NP-Complete
• Simplifying the signature in second-order unification
• Mechanizing Mathematical Reasoning

This page was built for publication: Decidability of bounded second order unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1887168)