Abstract

The amount of computerized information is increasing at a dramatic rate. More and more of that information is presented in graphical form. This poses a challenge to procedures which automatically process computerized information. This dissertation shows that one can build diagrammatic system in which to give valid proofs and that one can automate the process of giving such proofs. ;We define DiaPlan, a proof system for planning in the blocks world of artificial intelligence. The primary reason for selecting the blocks world is that people clearly prefer diagrams over sentential representations when it comes to solving problems in this domain. If diagrammatic reasoning has benefits over reasoning with sententially presented data, it should manifest here. ;We informally describe the domain to be modeled and explain how we plan to extend traditional formalizations of the domain. Following this, we define a mathematical model of the domain. In DiaPlan, diagrams are used to represent states and plans. Just as natural or artificial languages are made precise by defining a syntax for them, syntactic definitions for the diagrams used in our system are presented. The mathematical model of the domain is used to give a semantics for diagrams. Traditionally, a semantics is rarely given for artificial intelligence systems. It is important to give a semantics, as it enables one to define notions such as consequence. We explain the general set-up for proofs and discuss and define four kinds of proofs: consequence, nonconsequence, consistency, and inconsistency proofs. We show how they manifest in our system and explain how they enrich the kinds of problems that can be posed in planning systems. We define rules of inference for our system and prove them sound. Completeness is shown for a restricted class of consequence claims. ;Based on the logical system, we design an automatic theorem prover. We discuss how to best represent our diagrams on a computer, and present and discuss algorithms for the four kinds of proofs. In the conclusions, we briefly address how one could build general-purpose diagrammatic systems