Modular AC unification of higher-order patterns

DOI10.1007/BFb0016847zbMath1495.03016MaRDI QIDQ5096303

Zhenyu Qian, Kang Wang

Publication date: 16 August 2022

Published in: Constraints in Computational Logics (Search for Journal in Brave)

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Problems in rewriting III

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in abelian semigroups
• The undecidability of the second-order unification problem
• AC-unification race: The system solving approach, implementation and benchmarks
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Complete sets of transformations for general E-unification
• A Unification Algorithm for Associative-Commutative Functions
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Modular higher-order E-unification
• The Clausal Theory of Types

This page was built for publication: Modular AC unification of higher-order patterns