An Implementation of a Dissolution-Based System Employing Theory Links

We have been developing an automated deduction system based on path dissolution, an operation that was first introduced in [7]. Preliminary experimental results are promising. The next major phase in the development of that system will be the inclusion of a theory-link processor. In this paper, we describe those experimental results and some of the meta theory required for that next phase.