Decidable higher-order unification problems

DOI10.1007/3-540-58156-1_46zbMath1433.68562OpenAlexW1507462387MaRDI QIDQ5210802

Christian Prehofer

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_46

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

Regular Patterns in Second-Order Unification ⋮ A restricted form of higher-order rewriting applied to an HDL semantics ⋮ Tractable and intractable second-order matching problems ⋮ Higher order disunification: Some decidable cases ⋮ Higher order conditional rewriting and narrowing ⋮ Higher-order narrowing with convergent systems ⋮ Restricted combinatory unification ⋮ On the undecidability of second-order unification ⋮ Higher-order narrowing with definitional trees

Uses Software

• TPS
• Nuprl
• Elf

Cites Work

• Synthesis of rewrite programs by higher-order and semantic unification
• 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
• Third order matching is decidable
• Higher-order unification revisited: Complete sets of transformations
• Higher-order narrowing with definitional trees
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Decidable higher-order unification problems