A combinatory logic approach to higher-order E-unification

DOI10.1016/0304-3975(94)00210-AMaRDI QIDQ673971zbMATH OpenFDO

Authors Daniel J. Dougherty, Patricia Johann

Publication date 28 February 1997

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

Full work available at URL https://doi.org/10.1016/0304-3975(94)00210-A

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)

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

Cites work

• scientific article; zbMATH DE number 4041327 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 599028 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1142318 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 847980 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• A Short Proof of Curry's Normal Form Theorem
• A unification algorithm for typed -calculus
• Adding algebraic rewriting to the untyped lambda calculus
• An Efficient Unification Algorithm
• Axioms for strong reduction in combinatory logic
• Complete sets of transformations for general E-unification
• Conditional rewrite rules: Confluence and termination
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification via combinators
• Higher-order unification with dependent function types
• Modular higher-order E-unification
• Normal forms in combinatory logic
• Polymorphic rewriting conserves algebraic strong normalization
• Strong reduction and normal form in combinatory logic
• Termination of rewriting
• The decidability of hindley's axioms for strong reduction
• Unification in a combination of arbitrary disjoint equational theories
• Unification in a combination of equational theories: an efficient algorithm
• Unification theory

Cited in

(13)

• Higher order E-unification
• Normal forms in combinatory logic
• Theory and practice of minimal modular higher-order \(E\)-unification
• Rewriting, and equational unification: the higher-order cases
• Higher-order unification via combinators
• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 4047723 (Why is no real title available?)
• E-unification for second-order abstract syntax
• scientific article; zbMATH DE number 125880 (Why is no real title available?)
• One is all you need: associative second-order unification without first-order variables
• scientific article; zbMATH DE number 4053008 (Why is no real title available?)
• Modular higher-order E-unification
• scientific article; zbMATH DE number 1927411 (Why is no real title available?)

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)