Temporal Deduction in a Graphical Logic

Contents

Graphical Interval Logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have implemented an automated deduction system for Graphical Interval Logic that includes a graphical user interface and an automated theorem prover. The graphical user interface enables the user to create Graphical Interval Logic formulas and proofs on a workstation display, and the theorem prover checks the validity of deductions in the logic. In this paper we describe the logic, the automated deduction system, and an application to robotics.