REASONING ABOUT DEFINEDNESS － A DEFINEDNESS CHECKING SYSTEM FOR AN IMPLEMENTED LOGIC

Abstract

<p>Effective definedness checking is crucial for an implementation of a logic with undefinedness. The objective of the MathScheme project is to develop a new approach to mechanized mathematics that seeks to combine the capabilities of computer algebra systems and computer theorem proving systems. Chiron, the underlying logic of MathScheme, is a logic with undefinedness. Therefore, it is important to automate, to the greatest extent possible, the process of checking the definedness of Chiron expressions for the MathScheme project. This thesis provides an overview of information useful for checking definedness of Chiron expressions and presents the design and implementation of an AND/OR tree-based approach for automated definedness checking based on ideas from artificial intelligence. The theorems for definedness checking are outlined first, and then a three-valued AND/OR tree is presented, and finally, the algorithm for reducing Chiron definedness problems using AND/OR trees is illustrated. An implementation of the definedness checking system is provided that is based on the theorems and algorithm. The ultimate goal of this system is to provide a powerful mechanism to automatically reduce a definedness problem to simpler definedness problems that can be easily, or perhaps automatically, checked.</p>