| dc.contributor.author | Østvold, Bjarte M. | |
| dc.date.accessioned | 2022-10-18T17:07:09Z | |
| dc.date.available | 2022-10-18T17:07:09Z | |
| dc.date.created | 2004-04-01T00:00:00Z | |
| dc.date.issued | 2004 | |
| dc.identifier.uri | https://hdl.handle.net/11250/3026765 | |
| dc.description.abstract | In 1970 both Plotkin and Reynolds defined the anti-unification of a set of literal clauses, that is, atomic formulas or negated atomic formulas. They gave similar imperative anti-nification algorithms and proved the algorithms correct. We formulate an alternative anti-unification algorithm using recursive equations and prove its correctness. This functional-style algorithm gives a modular view of anti-unification, where each equation captures a different computational aspect. Modularity makes the algorithm well-suited as a starting point for designing related algorithms. It can easily be converted into a program in a functional programming language. | |
| dc.description.abstract | A functional reconstruction of anti-unification | |
| dc.language.iso | eng | en_US |
| dc.publisher | Norsk Regnesentral | en_US |
| dc.relation.ispartofseries | NR-notat; | |
| dc.relation.uri | http://publications.nr.no/3913/_stvold_-_A_functional_reconstruction_of_anti-unification.pdf | |
| dc.title | A functional reconstruction of anti-unification | en_US |
| dc.title.alternative | A functional reconstruction of anti-unification | en_US |
| dc.type | Research report | en_US |
| dc.description.version | publishedVersion | |
| cristin.ispublished | true | |
| cristin.fulltext | original | |
| dc.identifier.cristin | 957281 | |
| dc.source.issue | DART/04/04 | en_US |
| dc.source.pagenumber | 20 | en_US |
