This thesis describes Visual Logic (VL), a software tool for computing several new logical concepts introduced by John Fisher (the author's thesis advisor) [Fisher96] and graphically illustrating the result using clause trees. VL can also be used to visualize and animate (a restricted set of) logic programs and their execution; that is, as a graphical tracer for logic programs. The primary aims of the project are: 1) to implement and experiment with a prototype system; 2) to assess its effectiveness both as a computing platform for the new logical concepts and as a tree-based visualizer for logic programs in general; and 3) to propose specifications for an extended system. In addition, the thesis relates Visual Logic to similar diagrammatic and graphical systems utilized in logic.

Introduction

There are two main rationales behind Visual Logic (VL). The first is to support and enhance the work of John Fisher, who introduces the concept of supported propositions using formalizations based upon clause trees [Fisher96]. Supported propositions are defined as "relatively safe logical consequences of certain consistent sub-programs." Supported propositions and related concepts (to be defined later) are meant to provide a framework for dealing with logic programs which may be classically inconsistent as a whole but which may nevertheless contain interesting consistent sub-programs. While several Prolog programs written by Fisher were available for computing these new logical concepts, it became apparent that having a graphical system capable of displaying and possibly manipulating the associated clause trees would be both useful and instructive. Originally conceived as a mean of graphically showing "conflicts" in logic programs, VL eventually evolved into a flexible query engine and explorer of logical clause databases. To a lesser extent, VL can also be seen as a graphical tracer for certain logic programs. With further enhancements, VL can become a platform for visual logic programming.

The second rationale behind the project is to show how visual systems can be used to augment and enhance traditional symbolic representations in the field of logic. Humans routinely use diagrams to facilitate the process of design, reasoning, and problem solving. Researchers have shown that the use of diagrams plays several roles in this respect: as a short-term memory device, as a well-understood base concept from which more complicated parts of a problem may be described, as an aid in visualization, or as a tool in selecting an appropriate method or approach [Novak92]. The use of diagrams and other visual representations helps reveal important information that may not be apparent in sentential/linguistic or symbolic/mathematical forms [Tessler93]. However, except for a few notable exceptions, diagrams have been largely ignored by logicians and Artificial Intelligence (AI) researchers who have for the most part focused on symbolic representations and symbolic reasoning [IUVIL95].

Recently, there has been a renewal of interest in the use of diagrammatic or visual representations in problem solving and reasoning, typified by the recent AAAI (American Association for Artificial Intelligence) Symposium on reasoning with diagrammatic representations in 1992. The symposium brought researchers from various disciplines to discuss both psychological and AI-related issues. The consensus view emerging from the symposium was that "traditional symbolic representation will increasingly be combined with visual representation in future AI research" [Chandra93]. This is an important inspirational basis for the project.

The next chapter provides a brief survey of related works. Chapter 3 discusses the theoretical foundation of Visual Logic. Chapter 4 describes the functions of the current system. The last chapter provides an in-depth discussion of VL along with a comparison to similar systems and a proposal for possible extensions.