A combinatory logic approach to higher-order E-unification

DOI10.1016/0304-3975(94)00210-AzbMATH Open0874.68271MaRDI QIDQ673971FDOQ673971

Authors: Daniel J. Dougherty, Patricia Johann 

Publication date: 28 February 1997

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

Recommendations

• Higher order E-unification
• scientific article; zbMATH DE number 1088023
• Modular higher-order E-unification
• Higher-order unification via combinators
• Higher-order unification revisited: Complete sets of transformations

zbMATH Keywords

first-order equational theory

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• An Efficient Unification Algorithm
• Title not available (Why is that?)
• Termination of rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unification in a combination of arbitrary disjoint equational theories
• Conditional rewrite rules: Confluence and termination
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unification in a combination of equational theories: an efficient algorithm
• Adding algebraic rewriting to the untyped lambda calculus
• Title not available (Why is that?)
• Unification theory
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Polymorphic rewriting conserves algebraic strong normalization
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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

Cited In (10)

• Higher order E-unification
• Normal forms in combinatory logic
• Rewriting, and equational unification: the higher-order cases
• Higher-order unification via combinators
• Higher order unification via explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modular higher-order E-unification
• Title not available (Why is that?)

This page was built for publication: A combinatory logic approach to higher-order E-unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673971)