DFKI Technical Memo-91-02
by Knut Hinkelmann
Bidirectional Reasoning of Horn Clause Programs: Transformation and Compilation
A compilative approach for forward reasoning of horn rules in Prolog is presented. Pure horn rules - given as Prolog clauses - are to be used for forward and backward reasoning. These rules are translated into Prolog clauses, denoting one forward reasoning step. Forward chaining is triggered by an initial fact, from which the consequences are derived. Premises of forward rules are verified by Prolog's backward proof procedure using the original clauses. Thus, without any changes to the Prolog interpreter integrated bidirectional reasoning of the original horn rules is possible. Breadth-first and depth-first reasoning strategies with enumeration and collection of conclusions are implemented. In order to translate forward clauses into WAM operations several improvements are introduced. To avoid inefficient changes of program code derived facts are recorded in a special storage area called retain stack. Subsumption of a new conclusion by previously derived facts is tested by a built-in procedure. As a reasonable application of this kind of forward reasoning its use is demonstrated for integrity constraint checking.
This document is available as PDF-File(16,1MB).
The next abstract is here, and the previous abstract is here.
Note: This page was written to look best with CSS stylesheet support Level 1 or higher. Since you can see this, your browser obviously doesn't support CSS, or you have turned it off. We highly recommend you use a browser that supports and uses CSS, and review this page once you do. However, don't fear, we've tried to write this page to still work and be readable without CSS.