Higher order disunification: Some decidable cases

DOI10.1007/BFb0016848zbMath1495.03014OpenAlexW2160623077MaRDI QIDQ5096304

Denis Lugiez

Publication date: 16 August 2022

Published in: Constraints in Computational Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0016848

zbMATH Keywords

higher-order logicunificationlambda calculusdisunification

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 (2)

On solving nominal disunification constraints ⋮ Nominal equational problems

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Equational problems and disunification
• The undecidability of the second-order unification problem
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Higher-order unification revisited: Complete sets of transformations
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Decidable higher-order unification problems

This page was built for publication: Higher order disunification: Some decidable cases