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. Then the...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Discrete Mathematics & Theoretical Computer Science
2000-01-01
|
| Series: | Discrete Mathematics & Theoretical Computer Science |
| Subjects: | |
| Online Access: | https://dmtcs.episciences.org/270/pdf |