Decidability of bounded higher-order unification

DOI10.1016/j.jsc.2005.01.005zbMath1126.03017MaRDI QIDQ2456577

Klaus U. Schulz, Manfred Schmidt-Schauss

Publication date: 19 October 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

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

zbMATH Keywords

higher-order unification; simply typed lambda calculus; decision algorithms; exponent of periodicity; bounded unification problems

Mathematics Subject Classification ID

68W30: Symbolic computation and algebraic computation

03B25: Decidability of theories and sets of sentences

03B40: Combinatory logic and lambda calculus

Uses Software

• ML
• Haskell
• Miranda
• ETPS
• Curry

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• A unification algorithm for second-order monadic terms
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• The typed lambda-calculus is not elementary recursive
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Word unification and transformation of generalized equations
• Isabelle. A generic theorem prover
• Third order matching is decidable
• Proof theory and automated deduction
• Solvability of context equations with two context variables is decidable
• On rewrite constraints and context unification
• On the undecidability of second-order unification
• Decidability of bounded second order unification
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed λ-calculus
• Decidability of the unification problem for second-order languages with unary functional symbols
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Complexity of Makanin's algorithm
• Decidability of fourth-order matching
• Higher Order   Matching is Undecidable
• A Decision Algorithm for Stratified Context Unification
• Linear second-order unification
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• Automated Deduction – CADE-19
• The Clausal Theory of Types
• Makanin's algorithm for word equations-two improvements and a generalization
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item