The Interaction of Observation and Inference in a Formal Representation System

Abstract

This work is an attempt to formally represent the knowledge required for the solution of a difficult retrograde chess problem (figure I). This solution Includes the extension of a formal deductive system to Include an observational facility. Using a proof checker for first order logic. FOL [9], we have detailed a proof of the solution of the puzzle, Including proofs for almost all of the necessary associated lemmas [2], We shall highlight the various representational decisions made In the process of axiomatiiing retrograde chess, discussing both the necessity for these particular choices, and their Implications for designers of representations for other domains. This work is part of the search for epistemologically effective formalisms for artificial Intelligence.