0. Inference browsing with <= x X =>

Download and start GeologUI.jar and load the following theory. (Save the following code to file p.gl. Then drag the file to the theory pane, or use Open on the File menu. )
% p.gl

true => domain(X), p(X).

p(X) => q(X) ; r(X) ; domain(Y), s(X,Y).

domain(X) => u(X).

u(X), q(X) => false.

r(X) => goal.

s(X,Y) => goal.

Exercise: Duplicate the inferences in the following slide show using the GeologUI application (with p.gl loaded).

Start the web slide show demo by clicking HERE.
Use the arrows at the top of a slide to navigate inferences forward and backward.
At any time during the slide show one can return to this page by clicking on experiment ♦0 in the Geolog Experiments frame.

The depth-first geolog tree procedure ...

A rule binding is applicable provided that its antecendent matches facts on the current branch and none of the consequent choices of the rule (using the binding which satisfies the antecedent) are already satisfied on the current branch. Antecedent facts are matched left to right using the shallowest fact on the current branch (from the root true).

An applicable rule is used to expand the tree. Tree expansion continues at the leftmost branch. A branch is successfully saturated at a goal or false leaf, and extension of the tree continues at the deepest branch point having unextended choices (if any), and the first unextended branch is extended (if possible). A branch is unsucsessfully saturated provided that the branch does not have goal or false as a leaf and there are no additional applicable rules. A termination proof obtains if every branch is successfully saturated. Termination also occurs if the current branch cannot be extended and then the branch is a counter-model for the geolog theory.

The foregoing paragraph describes the standard depth-first procedure for building geolog trees. It corresponds to a particular kind of execution of the Skolem machine specified by the geolog theory. In the slide show this standard procedure applies if the user simply hits the infer button => every slide. The inference procedure can be altered using either x (next binding) or X (next rule), and this is illustrated on slide #10, producing a shorter proof. The next binding (x) seeks a new binding via backtracking on matches for the antecedent factors of the current rule, in the given order, from right to left.

It is possible to alter the depth-first inference procedure using various so called heuristic controls. Some of the current heuristic controls are described in other experiments. When heuristic controls are enabled, the manual controls <= x X => are disabled.