PhD Thesis, University of Tasmania, 1995

Abstract

We propose a broad system for reasoning by term rewriting. Our general aim is to capture mathematical and scientific reasoning in a coherent system. To this end we introduce several new processes which allow concrete descriptions of standard notions.

For deductive reasoning we extend traditional methods for finding canonical rewrite systems to a general method for systems involving both equations and inequations. We introduce the notion of side conditions for non-theorems and show how they provide a new kind of meta-reasoning whereby an automated reasoner can determine why it failed to prove a given statement. A method for the automatic proof of inductive theorems by an analogue of mathematical induction is also presented.

A new algorithm is given for inductively generating conjectures (function equations) from a set of observations (a rewrite database). This is a process of scientific induction and we prove some fundamental results linking it to mathematical induction. Comparisons are given with standard inductive learning systems, such as FOIL, to illustrate the expressive power of our algorithm.

We obtain probabilistic measures of the strength of a single conjecture using statistical testing and an information measure. For a collection of conjectures we are then able to quantify Popper's well-known falsifiability criterion for the strength of a theory. We also introduce a non-standard modal operator to extended our deductive reasoning to reasoning with conjectures.

We use belief dynamics as the framework of an implementation of the reasoning methods. Consistency analysis, using the same canonical-form algorithm introduced earlier, allows the reasoner to build a belief set from given knowledge and to form a working theory from the conjectures it makes. Again a meta-reasoning is introduced, with the reasoner then able to decide what experiments need to be carried out when it conjectures more than one consistent theory from given set of observations.

Dialogues with the reasoner, generated by a prototype implementation of the work in the thesis, are given to illustrate its behaviour and the links between the internal language it uses and natural language.