Modular higher-order E-unification

DOI10.1007/3-540-53904-2_97zbMath1503.68144OpenAlexW1494221669MaRDI QIDQ5055760

Zhenyu Qian, Tobias Nipkow

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) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Efficient second-order matching, Introduction to ``Milestones in interactive theorem proving, Modular AC unification of higher-order patterns, A combinatory logic approach to higher-order E-unification, Theory and practice of minimal modular higher-order E-unification

Uses Software

• LARCH

Cites Work

• Unification in a combination of arbitrary disjoint equational theories
• Matching - a special case of unification?
• Unification in combinations of collapse-free regular theories
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Complete sets of transformations for general E-unification
• Higher-order unification revisited: Complete sets of transformations
• Simplification by Cooperating Decision Procedures
• An overview of LP, the Larch Prover
• Combining matching algorithms: The regular case
• Unnamed Item
• Unnamed Item
• Unnamed Item