Modular AC unification of higher-order patterns
From MaRDI portal
Publication:5096303
DOI10.1007/BFb0016847zbMath1495.03016MaRDI QIDQ5096303
Publication date: 16 August 2022
Published in: Constraints in Computational Logics (Search for Journal in Brave)
03B35: Mechanization of proofs and logical operations
68Q42: Grammars and rewriting systems
03B40: Combinatory logic and lambda calculus
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
Cites Work
- Unification in abelian semigroups
- The undecidability of the second-order unification problem
- AC-unification race: The system solving approach, implementation and benchmarks
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Complete sets of transformations for general E-unification
- A Unification Algorithm for Associative-Commutative Functions
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Modular higher-order E-unification
- The Clausal Theory of Types
- Unnamed Item
- Unnamed Item
- Unnamed Item