Related works
The main areas of work which are important to
the thesis are:
- Classical logic and resolution.
- Logic programming paradigm in general and the
Prolog language in particular.
- Visual logic programming.
- Visualization of logic programs.
The logical concepts explored by VL are extensions
of classical logic and can be shown to be closely related to classical
satisfiability and logical consequence [Fisher96]. In addition,
they are defined through the use of clause trees, which closely
parallel resolution, the basis for mechanical theorem proving
[Chang73]. The close relationship to classical
logic and resolution lends robustness to these new concepts by
allowing well-known results to be applied to them.
VL contains an inference engine for logic programs.
As such, it has its roots in the logic programming paradigm,
the standard text for which is [Lloyd87]. In particular, Visual
Logic borrows elements from Prolog [Clocksin84] (e.g., unification
and backtracking) and also shares some of its limitations (e.g.,
lack of an occurs check). More importantly, it provides several
enhancements to standard Prolog systems, including computation
of newly defined logical properties, graphical presentation of
executing programs, and arbitrary selection of matching clause
during resolution and choice point during backtracking.
Visual logic programming refers to visual
programming languages with logic programming semantics as opposed
to procedural semantics. Two examples are Pictorial Janus and SPARCL.
Pictorial Janus [Kahn92] is a system constructed to visualize concurrent
programs and their execution but can also be used to produce animation
of Horn clause proofs. Pictorial Janus uses a highly pictorial
syntax in which the basic elements -- literals, clauses, variables,
constants, and terms -- are represented graphically. Input programs
are diagrams which can express Horn clauses, including variables
and terms. The semantics of the diagrams depends only on their
topology (i.e., size and shape are irrelevant except for readability).
Unlike similar systems which depend on some textual representation
of code, Pictorial Janus is capable of parsing Postscript description
of drawings. Its animation component attempts to prove the query
and, if successful, produces an animation of the proof that maintains
the style and conventions of the input diagrams.
SPARCL (Set PARtition and Constraint Language) [SPARCL93]
is another visual logic programming language. It is a logic programming
language in that the semantics of the language is based on resolution
of Horn-like clauses. It is a visual language in that the representation
of data is extensively graphical and programming in SPARCL largely
involves manipulation of that representation.
VL is not truly a visual logic programming language
since it uses a textual representation of clauses and allows only
limited manipulation of the output. VL resembles more closely
the systems for visualizing logic programs described next.
Various systems have been developed for visualization
of logic programs. These systems are designed to aid in learning
logic programming and debugging logic programs (Prolog programs,
in particular). An early example is Mellish's animated Prolog
tracer running on text terminals. The tracer was used primarily
to show beginning students the run-time behavior of Prolog. The
system is limited in that a) variables are destructively replaced
during instantiation, making it difficult to 'go back' and see
what happened; and b) it is only suitable for small toy programs
[Eisenstadt88].
In a similar vein, Bundy et. al. [Bundy86] propose a way
of 'telling a story' about the execution model of Prolog via an
AND/OR tree representation. Their work shows that in comparison
to other models (e.g., the Byrd box model [Byrd80]), the AND/OR tree model
has the greatest potential for clearly describing the execution
of logic programs. In addition, the model's simplicity makes
it especially suitable for teaching Prolog. An example of an
AND/OR tree is shown here, with AND denoted by horizontal bar.
Each node corresponds to a goal while its children correspond
to subgoals. The meaning of the tree is: a
is true if b, c,
and d are all true; c
is true if either e is true or both
f and g
are true.
Eisenstadt and Bradshaw [Eisenstadt88] continue these works
with the Transparent Prolog Machine (TPM), a graphical tool designed
for visualizing and animating the execution of Prolog programs.
Aimed at novices and experts alike, TPM is capable of showing
the Prolog execution model 'in gory detail' yet at the same time
enables the programmer to view the execution of very large Prolog
programs. In coarse-grained view, TPM uses the familiar AND/OR
tree representation, except that large trees can be vastly condensed
by collapsing large sections into user-definable 'black boxes.'
Program execution can be viewed live or retrospectively.
Through a VCR-like facility, the programmer can single-step the
code forward, backward, rewind, or play (execute) normally.
TPM coarse-grained (or long-distance) view. Source: [TPM93] (see also [Eisenstadt88]). Used with permission by Marc Eisenstadt.
For a fine-grained view, TPM utilizes what Eisenstadt
and Bradshaw call AORTA diagrams (And Or Tree, Augmented).
Each node in an AORTA diagram is a procedural status box
which includes complete details of unification and control history
for that node (goal). (A procedure refers to the collection of
clauses defining a single relation.) The upper part of the box
shows the goal's status - whether it is being processed (a question
mark), whether it has succeeded (a check mark), whether it has
failed (an 'X'), or whether it was successful but subsequently
failed upon backtracking (a check mark/'X' combination). The
clause number in the lower half of the box indicates which clause
in the procedure is currently being used. The 'legs,' or branches,
protruding under the procedural status box correspond one-to-one
to the clauses in that procedure. The small clause status
box in each branch shows the result of executing the corresponding
clause. It uses the same four symbols of the procedural status
box, with the same meaning. The clause status box may also be
a horizontal bar, indicating there is no matching clause.
TPM AORTA diagram in fine-grained view. Source: [TPM93] (see also [Eisenstadt88]). Used with permission by Marc Eisenstadt.
TPM is capable of showing variable instantiation
and propagation through arrows coming in and out of each variable.
Oval labels are used whenever arrows are not sufficient to show
where particular variables came from. Variable renaming is made
apparent through variable subscripts. TPM can also show extra-logical
features. For example, a clever visual metaphor (scissors and
clouds) is employed to show the effect and scope of the cut.
As mentioned earlier VL has the most in common with
the above systems for visualizing logic programs and their execution.
Where VL differs is in its focus. A detailed comparison is given
in section 5.6.
Though not directly related to it, there are many
on-going works that are of tangential interest to VL and will
be briefly mentioned here. For example, the Indiana University
has established the Visual Inference Lab (IUVIL), a multi-disciplinary
program aimed at understanding the role of visual information
in reasoning and developing tools that utilize visual information
in logic and reasoning [IUVIL95]. Among the projects developed there is Tarski's World, a graphics-based computer program that
uses a block world metaphor to teach students the language of
first order logic (FOL) and key concepts such as satisfiability
and logical consequence [Barwise91]. A similar system, Hyperproof [Barwise94], is designed to teach skills in analytical reasoning.
A basic aim of both systems is to show how visual as well as symbolic representations can be effectively employed in logic and reasoning. For an on-line demonstration, see [Tarski95] and [Hyperproof95].
Another world-wide, on-going area of research centers
on conceptual graphs -- a synthesis of existential graphs,
dependency graphs, and semantic networks. Existential graphs
were developed in the nineteenth century by the American philosopher and logician Charles S. Peirce as a system for showing logical relationships diagrammatically [Hart31]. Logical inference is performed directly on existential
graphs by copying and erasing graphs according to five rules of
inference and a single axiom. The versatility of existential
graphs is demonstrated by Sowa [Sowa93], who gives a
proof of the Splendid Theorem [((pr) (qs)) ((pq) (rs))] in
7 steps using Peirce's system. In contrast, the original proof
in Principia Mathematica required 43 inference steps and
28 references to other propositions.
In the 1970's, AI researchers combined existential
graphs with dependency graphs and semantic networks to create
conceptual graphs. Conceptual graphs are as general as predicate
calculus yet are as readable as special-purpose diagrams (E-R
diagrams, parse trees, Petri nets, etc.) [Sowa93]. Conceptual graphs have
attracted wide interest and research. A prime example is the
PEIRCE project, a multi-national effort to develop a "state-of-the-art,
industrial strength" conceptual graphs workbench. Taking
advantage of the widespread use of graphical workstations, PEIRCE [Ellis93]
allows developers to "write, draw, parse, and learn large
conceptual graphs / programs / databases / ontologies."
PEIRCE can be employed in diverse AI applications ranging from
natural language processing to adaptive chess playing systems.
[ Prev: Introduction | Next: Background | Up: Contents ]
luutran@cs.sci.csupomona.edu