|
|
Efficient Automata-Driven Subterm UnificationSyntactic unification has widespread use in computing. There are several operations used in deductive computing such as critical pair generation, paramodulation and narrowing that require unifying a term $s$ with every subterm of another term $p$. This subterm unification problem can be solved naively by repeatedly unifying $s$ with each subterm of $p$ in isolation. The drawback of doing unification in isolation is that commonality among subterms of $p$ is ignored . We present an algorithm for efficient subterm unification by exploiting this commonality. The central idea used in our algorithm is to reduce the common part computation in unification into a string-matching problem and solve it efficiently using a string-matching automaton. The automaton succinctly captures the commonality between subterms of $p$. The string-matching approach, in conjunction with two new techniques called bidirectional-reduce and marking enables efficient unification of $s$ with every subterm of $p$. |
|
Maintained by Sekar, sekar@cs.sunysb.edu |