Competing for theAC-Unification Race |
| |
Authors: | Alexandre Boudet |
| |
Affiliation: | (1) LRI, CNRS URA 410, Université Paris-Sud, Bât 490, 91405 Orsay Cedex, France |
| |
Abstract: | We describe our implementation of the unification algorithm for terms involving some associative-commutative operators plus free function symbols described by Boudetet al. The first goal of this implementation is efficiency, more precisely competing for theAC Unification Race. Although our implementation has been designed for good performance when applied to non-elementaryAC-unification problems, it is also very efficient on elementary problems. Our implementation, written in C and running on Sun workstations, is to be compared with the implementations in LISP, on Symbolics LIPS machines. |
| |
Keywords: | Unification equation solving logic programming automated theorem proving term rewriting |
本文献已被 SpringerLink 等数据库收录! |
|