Modular higher-order E-unification

DOI10.1007/3-540-53904-2_97MaRDI QIDQ5055760zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow, Zhenyu Qian

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-53904-2_97

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• Higher order E-unification
• scientific article; zbMATH DE number 1722699
• A combinatory logic approach to higher-order E-unification
• Theory and practice of minimal modular higher-order \(E\)-unification
• Higher-order unification via combinators

Cites work

• A unification algorithm for typed \(\bar\lambda\)-calculus
• An overview of LP, the Larch Prover
• Combining matching algorithms: The regular case
• Complete sets of transformations for general E-unification
• Higher order E-unification
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 4049025 (Why is no real title available?)
• scientific article; zbMATH DE number 4049130 (Why is no real title available?)
• scientific article; zbMATH DE number 4124996 (Why is no real title available?)
• Matching - a special case of unification?
• Simplification by Cooperating Decision Procedures
• The undecidability of the second-order unification problem
• Unification in a combination of arbitrary disjoint equational theories
• Unification in a combination of equational theories: an efficient algorithm
• Unification in combinations of collapse-free regular theories

Cited in

(17)

• Introduction to ``Milestones in interactive theorem proving
• Positive and negative results for higher-order disunification
• Higher-order unification via combinators
• scientific article; zbMATH DE number 1088023 (Why is no real title available?)
• scientific article; zbMATH DE number 1927411 (Why is no real title available?)
• scientific article; zbMATH DE number 1377612 (Why is no real title available?)
• Efficient full higher-order unification
• Rewriting, and equational unification: the higher-order cases
• Efficient second-order matching
• Modular AC unification of higher-order patterns
• Extensions of unification modulo ACUI
• Theory and practice of minimal modular higher-order \(E\)-unification
• Higher order E-unification
• E-unification for second-order abstract syntax
• A combinatory logic approach to higher-order E-unification
• Modular higher-order equational preunification
• One is all you need: associative second-order unification without first-order variables

Describes a project that uses

Uses Software

• LARCH

This page was built for publication: Modular higher-order E-unification

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