The Interaction of Observation and Inference

An intelligent computer program must have both a representation of its knowledge, and a mechanism for manipulating that knowledge in a reasoning process. This thesis examines the problem of formalizing the expression and solution of reasoning problems in a machine manipulable form. It is particularly concerned with analyzing the interaction of the standard form of deductive steps with an observational analogy obtained by performing computation in a semantic model. This dissertation is centered on the world of retrograde analysis chess, a particularly rich domain for both observational tasks and long deductive sequences. A formalization is embodied in its axioms, and a major portion is devoted to both axiomatizing the rules of chess, and discussing and comparing the representational decisions involved in that axiomatization. Consideration was given not only to the necessity for these particular choices (and possible alternatives) but also the implications of these results for designers of representational systems for other domains. Using a reasoning system for first order logic, 'FOL', a detailed proof of the solution of a difficult retrograde chess puzzle was constructed. The close correspondence between this 'formal' solution to the problem, and an 'informal, descriptive' analysis a human might present was shown. The proof and axioms were then examined for their relevance to general epistemological formalisms.