Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by Kirchner [14]. The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. The...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Discrete Mathematics & Theoretical Computer Science
2000-12-01
|
| Series: | Discrete Mathematics & Theoretical Computer Science |
| Online Access: | http://www.dmtcs.org/dmtcs-ojs/index.php/dmtcs/article/view/111 |