Visual Logic User Guide

Introduction

Visual Logic is a graphical software tool for querying and exploring logic programs. The main representation used are clause trees, which are somewhat analogous to proof or trace trees. The user interacts with the tool primarily in one of two 'modes.' 'Query' mode allows the user to make derivations from the clause database and optionally provides 'explanations' by showing the corresponding clause trees. 'Explore' allows the user to essentially trace the execution of logic programs by expanding and retracting arbitrary branches of the clause trees.

Visual Logic also performs computation of 'evident,' 'supported,' and 'conflicted' propositions. These logical concepts are introduced by Fisher as extensions to classical logic. They are meant to provide a framework for dealing with logic programs which may be classically inconsistent (unsatisfiable) as a whole but which may nevertheless contain interesting sub-programs that are in themselves consistent. For additional information, see

Fisher, John R., and Tran, Luu, A visual logic, Proceedings of the ACM Symposium on Applied Computing, 1996 (SAC96), Philadelphia, pp. 17-21.

Visual Logic was implemented using SWI-Prolog and the graphical package XPCE. Both SWI-Prolog and XPCE were developed at the University of Amsterdam and have been ported to various Unix/X11 platforms as well as Microsoft Windows (Win32s, 95 and NT). Visual Logic itself has been designed to run on any platform for which SWI-Prolog/XPCE is available.

Getting started

Starting the tool

After it is loaded, the tool is invoked by:
?- vl( <filename>).

The extension, by default, is '.vl' and may be omitted. Invoking the tool without an argument:

?- vl.

will open a file finder dialog from which the file may be selected. If a new (non-existing) file is specified, the user will be given the option to create it.

Format of the source file

The source file should be a plain text file consisting of clauses of the form:
p₁ | p₂ | ... | p_n <- q₁, q₂, ... , q_m . n > 0, m > 0.

or p :- q₁, q₂, ..., q_n . n > 0.

where vertical bars ( | ) represent disjunction and commas represent conjunction. Negation of a term is indicated by preceding it with a tilde ( ~ ). Otherwise, syntax for terms adheres to Prolog rules. That is, names and functors start with a lower case letter while variables start with an upper case letter. The underscore ( _ ) should be used in place of anonymous variables. Each clause must be terminated by a period.

Disjunction is allowed only in the head. Clauses whose implication operator is :- are added to the clause database unchanged. Clauses whose implication operator is <- are converted to a corresponding set of all possible contrapositive forms. That is, each clause

p₁ | p₂ | ... | p_n <- q₁, q₂, ... , q_m . n > 0, m > 0.

is converted to a set of m+n clauses

p_i :- ~p₁, ... ,~p_i-1,~p_i+1,..., ~p_n, q₁, q₂, ... , q_m . i = 1..n, AND

~q_j :- ~p₁,~p₂, ... ,~p_n, q₁, q₂, ..., q_j-1,q_j+1 , ... , q_m . j =1..m

Note that 'p <- true.' 'p :- true.' and 'p.' are all equivalent but 'p <- .' and 'p :- .' are not allowed.

The main window

The main window is a long narrow toolbar at the top of the screen. From here, the user can switch between the various windows, consult (load) a source file, edit the source file, invoke the help file, or quit the tool. (Note: the size and position of windows may have been changed by the local resource configuration file.)

The query window

Performing a query

To perform a query, type in a goal in the text entry field. Then, click on the Evdnt button, for example, to verify if the goal is evident. Similarly for conflicted and supported. As a short cut, clicking on the Query to first check whether the goal is evident and if so, whether it is conflicted and/or supported.

A goal may contain variables. In fact, typing in a lone variable X and clicking Query gives all possible derivations for the current program, For a large database, this may take a very long time to compute.

The tool responses to a query in one of two ways. If the goal fails, it simply returns a 'failed' message. Otherwise, it lists the results on the left pane of the window. A result may be listed more than once if there is more than one way to derive it.

Displaying the clause tree

Click on a result in the left pane to display its associated clause tree on the right pane. In effect, this provides an explanation for the answer. Each tree is displayed on its own white, raised area, called a 'cell.' The contingency set of each node is displayed in brackets ( [] ) to the left of its term.

Meaning of the different attributes (color and font style)

The attribute of each node (term) denote its value as follow:
• green: term is 'true' or ancestry resolved.
• blue: term is evident.
• bold and red: term is conflicted.
• bold and purple: term is supported.
• bold and black: conflicted and supported (i.e., moot).
• black: none of the above.

Important: a node's attribute shows its calculated global value and is not necessarily borne out by the tree it is in. That is, if a node is colored blue, then the node can be shown to be evident; however, it may not be the case that this particular tree shows that the node is evident. Also, the value of a node as shown is the most encompassing value that can be computed. Therefore, if a node is blue, then its term can be shown to be evident and no more, i.e., it is neither conflicted nor supported. It is also possible to show only a node's value according to the tree it is in, i.e., its local value (see below).

Mouse actions

Additional mouse actions in the query window:
• Click on a cell area: switch between showing global / local values.
• Click on a cell's label: minimize / unminimize the cell to hide / show the embedded tree.
• Click on a node: collapse / uncollapse node.
• Click on the canvas (drawing area): minimize / unminimize all cells.

Tip: right click on a result (left pane) or a node (right pane) to invoke the pop-up menu which gives access to all available commands. Also, place the mouse pointer over a button (in this or any window) to see a brief description of the button's function.