A combinatory logic approach to higher-order E-unification

DOI10.1016/0304-3975(94)00210-AzbMath0874.68271MaRDI QIDQ673971

Daniel J. Dougherty, Patricia Johann

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

first-order equational theory

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Normal forms in combinatory logic, Higher order unification via explicit substitutions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in a combination of arbitrary disjoint equational theories
• Termination of rewriting
• Conditional rewrite rules: Confluence and termination
• Unification theory
• Polymorphic rewriting conserves algebraic strong normalization
• Adding algebraic rewriting to the untyped lambda calculus
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Complete sets of transformations for general E-unification
• Higher-order unification revisited: Complete sets of transformations
• Normal forms in combinatory logic
• Higher-order unification via combinators
• An Efficient Unification Algorithm
• Higher-order unification with dependent function types
• Modular higher-order E-unification
• Strong reduction and normal form in combinatory logic
• Axioms for strong reduction in combinatory logic
• The decidability of hindley's axioms for strong reduction
• A Short Proof of Curry's Normal Form Theorem