Higher order disunification: Some decidable cases
From MaRDI portal
Publication:5096304
DOI10.1007/BFb0016848zbMath1495.03014MaRDI QIDQ5096304
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
03B25: Decidability of theories and sets of sentences
03B35: Mechanization of proofs and logical operations
03B40: Combinatory logic and lambda calculus
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
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