VL was implemented entirely in SWI-Prolog and the add-on graphical package XPCE. The choice of Prolog has advantages as well as drawbacks. On one hand, the construction of clause trees is more or less an extension of Prolog’s inference engine and therefore can be elegantly captured with a few Prolog rules. In addition, Prolog is well-suited for rapid prototyping. On the other hand, the use of Prolog imposes some limitations and difficulties of its own. This section discusses some pertinent issues in the design and implementation of VL.
p1 | p2 | ... | pn <- q1, q2, ... , qm . n > 0, m > 0.
is converted to two sets of clauses:
p1 :- ~p2,~p3,
... ,~pn-1,~pn,
..., q1, q2,... , qm
.
p2 :- ~p1,~p3,
... ,~pn-1,~pn,
..., q1, q2,... , qm
.
...
pn-1 :- ~p2,~p3,
... ,~pn-2,~pn,
..., q1, q2,... , qm
.
pn :- ~p2,~p3,
... ,~pn-2,~pn-1,
..., q1, q2,... , qm
.
and
~q1
:- ~p1,~p2, ...
,~pn, q2, q3, ..., qm-1,
qm .
~q2
:- ~p1,~p2, ...
,~pn, q1, q3, ..., qm-1,
qm .
...
~qm-1
:- ~p1,~p2, ...
,~pn, q1, q2, ..., qm-2,
qm .
~qm
:- ~p1,~p2, ...
,~pn, q1, q2, ..., qm-2,
qm-1 .
or, more succinctly:
pi :- ~p1, ... ,~pi-1,~pi+1,..., ~pn, q1, q2,... , qm . i = 1..n
and
~qj :- ~p1,~p2, ... ,~pn, q1, q2, ..., qj-1,qj+1 , ... , qm . j =1..m
The first formula yields n clauses and the second yields m clauses. Hence, the conversion produces a total of n+m clauses.
For example, given the following set of clauses:
a | ~b | c <- d, ~e. d <- ~f. ~e <- true.The above conversion produces:
a :- b, ~c, d, ~e. ~b :- ~a, ~c, d, ~e. c :- ~a, b, d, ~e. ~d :- ~a, b, ~c, ~e. e :- ~a, b, ~c, d. d :- ~f. ~f :- ~d. ~e :- true.For the last clause, ~e <- true. is equivalent to ~e <- . Since m=0, no conversion is needed. Note that even when the head of the clause is a single term (n=1), it is still necessary to convert the clause to its contrapositives in order to ensure that all inferences that could be made with the original set of clauses can be made with the resulting sets of contrapositives. To see why this is so, consider the following example:
Original clauses: 1) a|b<-true. 2) c<-a. 3) c<-b.
Contrapositives: 1) a:-~b. b:-~a. 2) c:-a. ~a:-~c. 3) c:-b. ~b:-~c.
Without at least one of the contrapositives { ~c:-~a,c:-~b }, it is not possible to show that c is evident via
Fisher calls such contrapositives back-links since they are used to "link back" to an ancestor [Fisher96]. Since according to classical logic each contrapositive clause is equivalent to the original clause, the conversion must be sound. However, a major problem with the conversion is that it leads to a large number of unnecessary clauses, that is, those which never lead to any useful derivation. Conceivably, a practical algorithm which performs some type of graph traversal can be devised to determine beforehand which back-links will be needed. The algorithm of course would have to employ some heuristics to avoid doing the work of inference engine itself! (As a trivial case, observe that if there are no clauses with disjunction in the head, then no back-links are necessary.) Since efficiency consideration was not a high priority, however, the current implementation of VL simply performs the conversion in full.
As an exception, VL adds any clause with a :- implication operator to the clause database as is. This allows for suppression of VL's automatic conversion of clauses to contrapositive forms at the programmer's discretion -- for example, in those cases when it is known beforehand that back-links are not needed -- thereby alleviating the redundancy problem. The other intended use for the :- notation is to denote utility relations (e.g., member/2) for which contrapositive conversion does not make sense or may lead to undesirable results.
P and Q are structurally equivalent if
Finally, Q subsumes P if, once all variables in P are bound with arbitrary atoms not occuring in Q, P and Q still unify.
For programs with no function symbols or programs which are completely grounded, the above test is guaranteed to detect infinte looping. For general programs with function symbols and non-ground terms, the test traps many but not all instances of infinite looping. Here is one example which fails: foo(X,1) :- ... , foo(1,X), ... . The subject of logic programs and loop detection is a difficult one in general. If at some later date, it is determined that VL should have a more rigorous method of infinite looping detection, see [Bol91] for an intensive work on this subject. Also, [Jones93] presents an algorithm for ensuring that a recursive literal in the definition of a predicate does not cause infinite recursion.
Query mode only shows closed clause trees. In other words, it lists on the left pane only terms that are at least evident. Also, when Query mode displays a clause tree, it calculates all possible values (evident/supported/conflicted) for each node and colors the node according to the most 'general' value. For example, a node colored purple is supported but not moot. A distinction is made between global and local values. A node's global value refers to its overall calculated value which is not necessarily borne out by the tree it is in, whereas its local value always pertains the containing tree. Hence, in a given tree, a locally evident node must have an empty contingency set, whereas a globally evident node may or may not. (If the latter case, then there must of course exist some other tree in which the globally evident node does have an empty contigency set.) By default, Query shows global values for nodes. However, the user has the option of switching between showing global and local values.
The implementation exploits XPCE's object-oriented paradigm. Conveniently, XPCE has built-in classes for hierarchical trees and nodes and provides standard methods for handling them such as iterating through the nodes of a tree, adding children to an existing node, and displaying the tree in horizontal or vertical layout. Each node in the explore tree is an extension of the generic node class and has attributes and methods that govern its appearance and behavior. In addition, each node object is associated with records that encapsulate all the information pertaining to it. This information includes the node's state, value, current term, used clauses, and variable bindings. To a large extent, operations in Explore mode are performed by sending messages to and among nodes. For example, when a leaf node determines it is 'true' or 'ancestry resolved', it sends a message to its ancestor nodes telling each to verify whether it is evident (at the root of a closed clause tree). The implementation seems to point toward the interesting possibility of applying objected-oriented paradigm to logic and inference, although the thesis will not pursue the details of this side issue.
VL represents the user's program clauses and terms simply as Prolog terms and treats them as data. As mentioned previously, Explore mode uses Prolog to perform head clause matching and unification. On the other hand, Explore must keep track of used clauses and variable bindings through each stage of tree expansion in order to uninstantiate variables and perform backtracking ('redo' in VL's terminology). The implementation details of maintaining variable bindings, performing variable propagation and uninstantiation, etc., are rather too complicated to delve into here. Instead, another difficult issue will be discussed next.
1) a( X, Y):- b( X), c( Y). 2) b( foo). 3) b( bar). 4) c( cat). 5) c( dog).
For the goal a(X,Y), the user should be able to get closed clause trees for {a(foo,cat), a(foo,dog), a(bar,cat), a(bar,dog)} in some order. Suppose the user expands the tree in depth first fashion as shown below (the number on the left indicates the order of node expansion; the set on the right indicates used matching clauses):
Next, suppose the user redoes node c(). (By default, the next unused clause -- c(dog) in this case -- will be used.) The tree then becomes:
Node c()is now 'exhausted' (both matching clauses have been used). Next, the user redoes node b(). What should be done with node c() at this point? Arguably, it should be left alone since its term is not affected. The tree is now:
Now all nodes are exhausted, but one derivation, namely a(bar,cat), was missed. Obviously, the user needs to be able to somehow 'reuse', as it were, the matching clauses {4,5} for c(). One possible solution is to allow the user to manually select arbitrary matching clause when expanding / redoing nodes. Some mechanism can be employed to display all available clauses for a given node and to indicate which clauses have been used. The user then has the option of using a new or used clause. A serious drawback of this approach is that it places on the user the onus of having to keep track of the different combinations of used/unused clauses in order to extract all solutions. Clearly, this is not feasible with any but the smallest trees.
Next, consider a different approach. Suppose when node b() is redone in the final step, node c() is 'restored'. In VL's terminology, 'restoring' a node entails 1) resetting its term to the value to the point prior to the initial node expansion; and 2) resetting its set of used clauses to empty. This leads to the tree below. The user can now expand and redo c() to get a(bar,cat) and a(bar,dog) as desired.
Again, the possibility of leaving it up to the user to manually perform 'restore' was considered and rejected as being too cumbersome. Instead, when a node P is redone, Explore mode automatically restores any node in the tree which was initially expanded after P. ('Initially expanded' refers to either the first instance the node is expanded or the first instance it is expanded after having been restored.) Note that Explore mode does have options for manually selecting a matching clause during expand/redo as well as manually restoring a node. However, the options are provided to give the user additional flexibility; they are not relied upon as a mean for obtaining all derivations.
In any event, the automatic restore feature is only part of the solution. Returning to the previous example, suppose the user expands then redoes node b() without ever expanding node c(). The (non-closed) clause trees obtained thus far are:
Subsequently, expanding and redoing c() only give closed clause trees for a(bar,cat) and a(bar,dog). b() will not be restored since it was initially expanded before c(). The problem in this case is that the tree was not completely expanded before the first redo. In fact, it can be shown through more complicated examples that in order to guarantee that all possible closed clause trees are obtained in Explore mode, the following rules must be observed:
Explore mode provides a way for expanding and redoing nodes specifically designed to accommodate the above rules. The user can ensure that there are no unexpanded nodes before doing a redo with the 'Expand tree from root' command ('0' key). Likewise, using the 'Redo last' command ensures that the last node expanded is the first redone. Incidentally, the user can emulate Prolog's execution model by using only these two commands to expand and redo nodes.
Finally, a couple of points should be kept in mind. First, VL provides an easier and faster way of getting all derivations via Query mode. Therefore, being able to do the same in Explore mode is perhaps more important for the sake of completeness and less so from the point of practicality. Second, 'Explore' would seem to imply that the user is less interested in finding all derivations than in investigating pertinent parts of the tree -- a task Explore mode is better suited for