The Interaction of Observation and Inference in a Formal Representation System

I. Introduction

2. Inference

Our consldenttlon centers on a particular retrograde chess puzzle (figure /). Its solution (from basic chess principles) Is beyond the ability of any current computer program.

figure I

This problem was chosen because Its solution "requires" both "deductive" and "observational" inferences, In a conteKt Isolated from other issues of correctne55 and sufficiency. Deductive Inference Is obtaining new proof steps by the application of syntactic inference rules. However, human reasoning proceeds not only by deduction, but also by the Immediate recognition of rtsults, a process we Identify with obmvation. We have extended our representational system to Include observational Inference by performance of computation In a umantic modtl.

* Author's current address: Department. of Computer Science, Indiana University, Bloomington, Indiana 47401.

** This work was supported in part by D-ARPA under contract MDA903-76-C-0206.

Human problem solving has several different modes. People are capable of deduction, applying syntactic rules to previous inferences. This has been the reasoning mode most frequently employed in A.l. programs. However, generally intelligent ~y~tems will need to reason by other schemes, such as tndttctlon (reasoning from particular cases to a general conclusion), analogy (modifying reasoning from a solution of another problem to fit the current situation), and what we call obwvafion (quickly noticing an apparent conclusion, performed in our system by computation in a semantic model). If we are to create such programs, we must find a pragmatic representational mechanism, one that can support these other kinds of reasoning.

We perceive that the general A.l. problem is better approached by separating the representation of the knowledge of the problem domain (epistemology) from the search mechanisms used to manipulate that knowledge (laturistics). This distinction is discus~ed more completely in ['/].

Classically, an axiom system is epistemologically adequate for solving some problem if there exists a solution of that problem from those axioms. For example, a world view based on Interacting particles would be classically adequate. AI, intent on the production of intelligent programs, makes greater demands on its fundamental knowledge structures. We require not only the generality of adequate systems, but also economy of expression; that the solution be not only derivable, but that the derivation be short enough for a machine to actually produce it. We call this notion of both economical and adequate formalisms epistemological effictivenm.

This paper is primarily concerned with the qualities OF formalisms capable of epistemologically effectively representing both complex deductive and observational reasoning.

Deduction is obtaining conclusions by application of syntactic rules. The term observation is usually applied to human inference In several ways; they are unif1ed by the notion of drawing a quick and Immediate conclusion by examination.

Examples of human observation are see~ In the technician reading the value of a meter, the mathematician recognizing the value of some simple function, and the clerk finding the amount of some transaction In a table.

This examination employs the following scheme: knowl~dge which Is to manipulated in deductive form 1s represented m a extended first order logic formalism. Associated With this log1cal system Is a computational LISP model of these ax1o~s. The results of the evaluation of functions on ob ;ects m thiS model are to be legal inferences in the deductive, logical system. This shall serve as our notion of observation. From the point of view of our Intelligent computer, observation by computation in a semantic model is as opaque as sensory input.

3. Basic Formalisms

Just as our use of "English" Is fundamental to our ability to present this raper, we have a fundamental need for an epistemologica language for expressmg reasonmg. For that, we have chosen an extended first order logic. It is the usual predicate calculus, with the addition of equality, functions, axiom scltemata, and Inference by computation in a semantic model.

We use formal logic for several reasons: I) The sentences of logic are unambiguous and easily understood. 2) F1rst order logic has explicit quantification. 3) There has been much work in logic. Any system employing logic can avail Itself of this work. Examples of such progress include resoluti~n and decision procedures for propositionaly log1c. 4) Log1c Is a general representation. It is obviously not contnved for one particular domain. 5) Declarative represen~atlons in ~eneral, and first order logic in particular, are eas1ly_ and umformly extensible. They can be extended not only w1th new ax10ms, but also with new predicates, functions and individuals.

These, however, are the minor justifications for the use of logic. More importantly, 6) First order logic provides a _precise sense of meaning. From the rules of mference mherent In the system it Is clear what can be deduced from any axiom. 7) Almost all other current representations, be they microplanner, semantic nets, K R L, or whatnot, are variations on the rules of formal logic. They are all expressible in logical terms . . These formalisms differ principally in their interaction with the heuristic system. They are all declarative systems, and (almost) equivalent in terms of epistemology. Rehance on pure log1c has two positive attributes: we are 1solatmg the epistemological Issues from the lmplementiltlon, and we are speaking the lingua franca of representation languages.

4. Proof General ion and Proof Checking

An intelligent computer l>rogram will need ~oth an epistemologically effective word vi~w and an apj)ropraate set of heuristic procedures. This reasonmg program as beyond our current abilities. However, we do not need this reasoning program to judge candidate epistemological formalisms. Rathrr. we need only to have our deductions certified. Clearly, the ability to accept a valid deduction is a prerequisite to the actual generation of that deduction. And an epistemologiCally adequate formalism can be tested by the use of a proof checker. This is essentially the Missouri p~ogram of McCarthy.Hayes [G), and is In the tradition of the Aclv1ct Taker [5).

We were fortunate to have available for this research the program FOL [1,9), an extended natural deduction . proo~ checker for first order logic. FOL will act as our MJSsoun program, checking the validity of our candidate inferences.

FOL Is a proof checker for an extended sorted first ord~r logic. FOL has been extended to incorporate a tautology dwder for propositional logic with equality. And, ~ore lmp?rtantly m FOL one has the ability to create a parttal umantiC model of one's world , and to evaluate the values of functions and predicates in that model, returning the results to the deduct1on level. This is called semantic simplification. ThiS ability IS satisfactory for simulating our notion of observation In chess.

5. Cheu Puzzles

At the beginnin£ of this paper, we mentioned a certain chess puzzle (figure l).'fl< While space llm1tat1ons preclude descnb111g the solution of that puzzle, the reader should notice that, not only is the solution very complex, but . that II also requtres at least two different varieties of reason1ng. Any solut1on Will exhibit both deduction, inference of the form "Both sides can't be in check at the same time, black is in check, therefore .~bite is not in check", and observation, inference of the form I see black is in check" . We perceive our task as finding the appropriate Incorporation of this observational reasoning into the deductive framework .

If the reader himself solves the puzzle, he will surely perceive how complicated chess reasonmg can be. In addition . to complexity, chess (as a problem domam) has another appealing attribute: we can wtcqu.ivoca/ly solve this problem. Th1s serves to help us to isolate the interesting features. And chess Is a somewhat ill-structured domain, the result of historical development, rather than mathematical . sparsity or . toy simplicity. Our results, therefore, Will pnnCipally be conce1 ned with mechanisms, not representatiOnal deta1ls. However, understanding these mechanisms requires the presentatiOn of those details.

We will employ two different forms of inference in our systemi the standard deductive methods, based on ax10ms and natura. deduction and augmented with decision procedures, and obse1vation: semantic simplification performed by computatiOn on a partial semantic model. We call this set of functions and data structures the Chess Eye. After defining a vocabulary of chess notions, we will consider the chess eye in greater detail.

G. Objects of lhe Chess World

Space limitations preclude . detailing the entire chess ax iomatization. Instead, we Will describe only a few of the more important and inttresting components.

The most obvious chess object is a chessboard, one of the Boards. Most chess problems are stated In terms of a board. Similarly, there are 6-4 Squares on any board, ~ach With a unique identity, and 13 possible Values, such as whtte pawn and empty, corresponding to the obJects on these squares.

However values are different than the chesspieces themselves; che whit~ queen's knight is not the same as the white king's knight; a promoted pawn is not the queen. Our reasonmg Will need these distinctions. Hence, we need a set of the 32 chessmen, called the Pieces.

The above, while somewhat sketchy, ought to appear fairly natural. However, as a representational mechanism, they are inadequate. We need to speak of the various things that must have happened to reach this point in the game, the capture that must have occurred, and so forth. Even the chess rules, In delimiting castling moves and draw conditions, refer to the entire game history. We therefore need an explicit set of historical states, the Positions, which can be though of as the history (set of moves) employed In reaching this particular board. (There will be many different games that could reached any particular board.) Positions are a variety of state vector; the reader Is referred to [6] for a more complete exposition on state vectors.

* The fallen piece in figure 1 was the whi_te queen~s bishop. The reader is referred to [2) for the deta1led solut1on.

There Is also the natural notion of the Moves, the explicit, discrete transitions betwten the positional states, and the Colors, black and white, associated with the two chess armies.

7. Predicates and Functions on Positions

Our most Important manipulations will Involve the state vectors, the positions. And the most fundamental relationship ln reasoning about chess ls that of legal move. Hence, we have the predicate SUCCESSOR(pl,p2) defined on two positions, If p2 can be reached by a legal move from pl.

If SUCCESSOR Is to be the succession function of our system, then, like arithmetic, we want a notion of "less than". This is called PREDEOAME. PREDEOAME(pl, p2) Is true when pi occurred in the game that reached p2. Naturally, the initial position, PO, has the PREC>EOAME relation to every legal game.

As each piece has its own Identity, we can refer to the piece occupying a given square In a particular position. Thus, lf px Is a. position that was played to reach the problem board, we have Pos(px, BI<RI)- WK. (Or, on BI<RI in px is the WI<)

We also have functions which extract the last move from a position, and the actors used in that move (Movt, Mover, To, From, Taken).

8. Prtdica.tes and Functions on Boards

Now, position$ were only one variety of state vector. The other, perhaps more familiar, sort is that of BOARC>S. Just as one can speak of the status of some square in some position, one can take the value on some square ori a board (VALUEON (GIVEN, DQ2) · RI-V). (Note, however, that the range of this function is Values, not P leces.)

The Issue of legal moves is also Important for boards; we have, for each piece, a predicate the determines the validity of any particular move for that piece on that board. Thus, for example, a bishop-valued piece can move from BQI to BI<BJ on board b only if l>IAG(b,BQI,BI<BJ) is true on that board. We can take the composition of these various movement types, and talk about MOVETO(b,v,sql.sq2) if, on board b, a piece of value v could move from square sql to square sq2. However, legality of move Is not purely a function of board; capture en passant and castling are not determined solely by board configuration.

Chessboards, as described in the previous section, will not even serve to represent the problem of figll.re I. Consider the square with the X upon it. It has no representation within the system of ordinary values that we have described. We resolve this difficulty by the introduction of a new constant, of type Values, one that stands for "I don't know what's here, but it is someth ing." This is the constant UD (for "undefined" value.) Permitting an undefined value to be on the squares _of boards creates a natural ordering on boards by greater defimtlon. We call this ordering SUBBOARD(bl,b2).

We need to tie boards and positions together. Obviously, a board with no undefined squares is the result of playing out a position. The function that extracts this board Is Tboard. We state that Vp b.(BOARD(p,b) · SUBBOARD(b,Tboard(p)). In reasoning about chess puZlles, we typically take the problem board, and Infer properties of any position that has the BOARD relation to it.

9. Observation in the Chess World

In our definition of the FOL inference system, we allowed computation in a partial semantic model to be a legal inference. We therefore define a LISP representation for (some) of the objects of our chess world, and to declare LISP functions to compute the computable predicates and functions on that model. For example, in our LISP model, atomic individual constants, like the black king and the white queen's bishop are LISP atoms; chessboards are eight long lists of eight atomic values.

Attachments are then made to functions and predicates such as VALUEON, ORTHO, and MOVETO. For example, the predicate MOVETO, which is defined axiomatically as:

Vb v sq1 sq2.(MOVETO (b,v,sq1,sq2l·

((VALUER(v )1\0RTH()(b,sq 1,sq2))v(V ALUEB(v)I\OIAG(b,sq 1 ,sq2))v

(VALUEQ(v)I\ORTHO<b,sq 1 ,sq2)) v(VALUEQ(v)I\OIAG(b,sq 1,sq2))v

(VALUEK(v)I\KINGMOVE(sq 1,sq2))v

(VALUEN(v)I\KNIGHTMOVE(sq 1 ,sq2))v

(VAL UEP(v)I\PAWNMOVE(b,v,sq 1 ,sq2)))),

is attached to the function:

MOVETO (LAMBDA (b v sq1 sq2)(COND ((VALUER v)(QRTHO b sq1 sq2))((VALUEB v)(DIAG b sq1 sq2))

((VALUEQ v)(OR (ORTHO b sq1 sq2)(DIAG b sq1 sq2)))

((VALUEK v)(KINGMOVE sq1 sq2))

((VALUEN v)(KNIGHTMOVE sq1 sq2))

((VALUEP v)(PAWNMOVE b v sq1 sq2))));

in. the semantic model. We build up our hierarchy to have predicates such as BLACI<INCHECK (which determines if black Is In check on a given board), computable In the chess model. Thus, though our system Is capable of expressing complex statements about chess, It Is still able to derive the fact that black Is in check on the problem board in a single inference.

The semantic simplification mechanism also has the ability to check WFF's quantified over finite sets by case computation in the semantic model. For example, the theorem: V x. 3 sq. Pos( PO,sq) - x (every che~spiece was on some square In the initial position) required 165 steps to derive deductively, but only a single semantic simplification.

This use of procedural computation In a model is a form of observation; the intelligent program, whose internal language is the formal predicate logic and axioms, can use the same mechanism for simplification done in its semantic model and observed events in the real world. What we are providing here is a mechanism for perception; that its primary usc In computers will be a form of internal visualization or hallucination Is no more a problem than accepting the human use of intemal visualization in human problem solving.

10. A X I oms

The most important axioms in this system are those that delimit legal moves. For example, consider the following representative axiom, MCONSEQ.A (move consequences A):

axiom MCONSEQA: Vr q.(SUCCESSOR(r, q)::~ ((~WHtTETURN r·WHTETURN q)I\~POSITIONINCHECK(q,Color r)l\ Prevpos q·ri\(WHITEPIECE Mover Move q·WHITETURN r)l\ Pos(r, From Move q)·Mover Move q 1\ Pos(q, To Move q)· Mover Move q 1\ Pos(q, From Move q)·EMPTY 1\ (CAPTURE Move q :::~ Pos(r, To Move q)·Teken Move q) 1\ (CASTLING(r ,q)vEN_PASSANT(r ,q)vSIMPLELEGALMOVE(r ,q))));;

It states some conditions on legal moves; which side Is on move, not leaving one's king In check, where the pieces In the move are, and the beglning of a taxonomy of move types.

It Is also Important to talk both about what remains true between moves. For example, those squares not Involved In the move retain the same contents between any position and its successor.

axiom MCONSEQO:

Vr q sq.((SUCCESSOR(r,q)l\ ~sq·From Move qA~sq·To Move ql\ ~(CASTLE Move ql\(sq·Aisofrom Move qvsq·Aisoto Move q))l\ ~(ENPASSANT Move qi\Sq·Takenon Move q))::~ Pos(r, sq)·Pos(q, sq));;

II. Chess Induction

Another feature of the chess axiomatization that deserves mention, Is CAess Induction. Chess induction Is an axiom schema that states that If a property P Is true of a position p, and remains true over the successor relation, then It will be true jn all descendants of p (all games that can be reached from p>.

We usually use the Initial position, PO, for p, and prove properties true of all legal positions. More formaf, this Is:

(P(PO)A V r p. ((P(r)A SUCCESSOR(r, p))::~P(p)));:, V r. P(r)

Chess Induction Is a useful deductive method. For example, using chess Induction, we prove theorems such as: A pitct not on its original squcm laas moved In tlals gamt (or bun tlat moving root of a castle):

V r sq x. ((Pos(r, sq)·XA .,(Pos(PO, sq)·x));:, J q.( (PR EDEGAM E(q,r)Vq·r)A((Mover Move q·xATo Move q·sq)V (CASTLE Move qAAisomover Move q·xAAisoto Move q·sq))))

And that bislaops sta' on a single color square:

Vr sql ~q2 ybi.((Pos(PO, sql)·ybii\Pos(r, s'l2.l·ybJ);:, (WHITESQ.UARES(sqi)·WHITESQ.UARES(sq2)))

This Is a powerful technique for dealing with the frame problem. If we have control over the types of lntera~tlons available in state transitions, Induction schemas such as thas one allow us to prove constant properties of distant states.

12. The Proof

This has been just a small sprinkling of examrles from the chrss axiomatizatlon. We hope it has been usefu In conveying their flavor and form. From this axiomatizatlon, we preceded to generate a proof of the solution to the chess puule.

The proof Itself Is too long to detail, but we are able to present a few comments about its "shape". The form of the proof matched, fairly closely, an English explanation of the detailed solution to the same problem. The human proof requared 68 "steps"; the FOL "proof", i05. In the process of deriving the FO L proof, 159 general chess lemmas and theorems were proven. These required I ?02 steps. Additionally. six lemmas specific to this problem were also demonstrated, requiring another 136 steps. A bout half of the proof steps in the main proof were Instantiations of axioms and theorems, and another quarter were requests for the confirmation of the chess eye. The complete FOL proof may be found In [2].

1:4. Syntactic and Semantic Reasoning

We will attempt to convey some of the epistemological design concepts uncovered In this examination. This Is a bnef description; a more thorough exammataon may be found In [2].

One of the major distinctions underlying this work Is that knowledge can be successfully modeled in two different forms. One Is by the application of s,ntactlc rults and the other, modtl bastd semantic computation. From the perspective of the perso.n communicating with a representational system, synta.cuc mechanism$ convey by their jom1 the Information (and passable uses of that information) they represent. Thus, in our system the axiomatic knowledge as syntactic. Knowing the rules of Inference, It is clear what is derivable from any axiom.

Semantic rules, on the other hand, are magic. We are not told the justification for any rule, why H works . how it works, o~ly that we are to accept its results. Typ1cally, 11 w1ll be performmg this action by functional evaluation in some partial model of the domain, complete with hidden assumptions about what Is right and possible there. Such inference is performed m this system by the functions of the Chess Eye.

Detailed exploration of formal chess reasoning reveals that It Is a fallacy to believe a simplt mttltodolop will be able to express the knowledge of a complex domam. . Expressmg complex relationships will require complex hnguasuc machmery. For examr.le, any systt'm dependent upon viewmg only a single mode. updated with each action, will be unable to compare states resulting from different act1ons In anyt~.mg but the most primitive way. Any system that thinks that a shortest path net traversal" algorithm will permit it to avoid dealing with inconsistency Is going to be unable to do deep reasonmg that relies on disjunction or case analysis.

14. State Vectors

The manipulation of state vectors played the central role in this axiomatization. State vectors are like the pract1ce of proofs In formal logic. Everyone knows how they can be used, but no­ one Is every caught manipulating one In a complicated way.

We remind the reader that there were two flavors of state vector employed in this research; the first is the static vector, the boards. Boards were used to display a particular slice of time. Similarly, these chessboards were a fully realized, concrete object upon which calculations could be performed. The second Is the historical vector, the posataon. A posltton contams the complete history of any particular game. However, It has no explicit representation In the model.

Each of these had Important application. The full realization of the board (the association with any board with a data structure that completely defined that board) permited computation on that board; and this employment of the Chess Eye proved remarkably useful In reducing the magnitude of derivation. However, the historical state vector, the position, was also vital. Much of the work of this proof consisted of comparing states, asserting that a particular state with particular properties must have existed. Usually this state occurred In the game played to reach some other state, and was interesting for that reason.

There is a third kind of state vector, the possiblt lllorid. This vector contains Information not only about the status of objects in the world, but also propositions about the propositions about those worlds. The most common use of these possible worlds is in semantic modeling of model logic systems. Possible worlds were not needed to model the simple world of retrograde chess.

State vectors seem to be one of three possible approaches to the problem of extending the set of things one can talk about in a formal system. This is the method of rtification, or the making of new objects. Here we postulates new, "ordinary" objects, from which propositional Information can be obtained by use of the axaoms. These objects can be manipulated by the use of the ordinary rules of the standard logic.

A second possible alternative is provided by modal logic formalisms; these attempt to talk about propositions by adding new "quantifiers" on propositions, and new inference rules to the deductave system. Unfortunately. if the proposition to be talked about contains several possible modals, the system can become rather cluttered with additional inference rules. And each additional modal requires extending not only the inference system, but also the heuristic system.

The third alternative focuses on the notion of meta ltvtl reasoning. That is, the propositions on one level become the ob jccts of the next level. An additional set of inference rules is required for transferring between these levels. Since this scheme can be recursively apphed, no additional mechanisms need be added to handle other proposition types. This is essentially a more advanced form of reification.

Of these three, the third seems most promising, and it is cu rrently being incorporated into FOL. If this axiomatization were to be rt>peated, the features of this meta level reasoning would have allowed more "incompletion" in the manipulation of the semantac model. However, the state of FOL at the time this research was performed compelled the use of reincatlon and state vectors rather than this last, more general scheme. These distinctions are discussed more fully in [10].

One other major success in the use of state vectors ought to be ml" nt ioned: we had great success applying induction schema to histor ical vectors to prove properties of distant states. The mduction schema Chtss /nductio11 stated that if a property was true over the successor relation, then it held in all descendants of an y state for which the property Is true. Chess anduction pctmited the proof of many previously lntranslent theorems, such as "Only pawns can /romote" and "Every piece now on some squa re eitiH'r move there in a previous position, or started on that square". We believe that this induction schema provided a good partial remedy to the frames problem, permitt ing proofs about distant states without even the trouble of simulating the actions involved.

I !i. Com pound Oh jects

T he state vectors ~re examples of another form of reification, t h ~ t of c r~a t ing compound ol1tcts. The mathematical comprehension principle, creating sets, lists and bags, are forms of compound obJects. Our experience is that compound objects play a critical role in even the simplest epistemology.

Compound objects are related to the idea of partially dtfintd ol1ects. A partially defined object is one that Is a representation for something we have conceptually more information. We suggest there are two different varieties of partially defined objects that need to be dealt with in a complex reasoning ~ystem . One of these Is exhibited by the boards with their explicit use of UD, the "undefined" constant. A board with an undefined In it is not conceptually a first class object of our system; rather, It Is an explicit representation an object about which we only have partial knowledge. This is its tremendous advantage; with this explicit representation, we can use a partial board as data for a functional evaluation. However, the use of this explicit undefined limits the set of things that can be unknown about a partial board; we might know that an undefined square contains some officer, or that there Is a queen somewhere on the board, or that this board was a legal move away from some other board. None of these partially defined obJects is representable by this scheme. Each of them could be represented by some other scheme, but not all sucl& partial information can be represented by any scheme that does not represent Its information propositionally. Representing propositional information in the model is already meta­ reasoning [10].

The alternate variety of partially defined objected exhibited In this representational system is the position. In one sense, the position is completely defined; the position does not have any formal elimination of Information. On the other hand, except for the most trivial positions, one knows nothing about any position that cannot be established prepositionally. It is only possible to Infer properties of a position from Its relation with other positions and boards.

We see then that the board Is the concrttt realization of the abstract position. Any epistemologically effective system Is going to need to deal with both abstract objects (for which there can be no representation In Its model) and concretions of those objects (for its model to manipulate).

This discussion leads us to touch upon the Issue of multiple representations or the different aspects of similar objects. What we are considering here is the ability to refer to objects that have a common conceptual source In different fashions.

We see this division In our chess axioms. Inherently, there Is only one conceptual object associated with any square at any point. Nrvertheless, we find the necessity for dealing with this object in two different garbs: piece and value. We essentially have things to say about the pieces that b,oth abstract information out (it's a white rook, not the white queen's rook) and that add Information in (but It used to be a pawn). We see this same division in the board/position duality, where the board Is really a "slice" of a position.

16. Linguistic Centrality

This final section provides a perspective on how well we've provided a language for reasoning about chess. We need to consider a two part perspective: What were the failures In this representation system? How well could it be used to talk about problems other than "A piece fell off the board ... ?"

There are two important linguistically failings In this ax iomatization. The first of these was the failure to Include general notions of comfJound objtcts, particularly sets and their kin. It was possible to deal with arguments equivalent to the "pigeon-hole principle" by case checking; but these are not naturally case arguments.

The other source of regret Is that the representation system, partlculi!rly In the semantic model, Is tied too closely to the rules of legal chess, and too closely to too simple an Idea of representing chess knowledge. This point can be better Illustrated with a pair of examples. Consider this problem:

The current axlomatitttlon, as currently formulated, would not recognize this "fragment" as a piece of a "board". However, this Is a natural extension for the human problem solver. The ax lomatltatlon can be criticized for adhering too closely to the rules of chess, i!nd Ignoring Its "primitives". Correction of the axlomatltatlon to reflect this more primitive level would not need to be a major a reviSion.

This second exi!mple dlspli!ys a more fundamental linguistic difficulty. Consider this problem, from [5~ somewhat more conventional In Its phrasing.

figurt J

This Is not so much an Issue of milling In four, so much as recognltlng thilt (as the black king and queen are on the wrong color squares) the pieces have exchanged sides. While the current iiXIomatlzatlon could be used to prove that If rvhltt started at tht bottom o1 this board, thtn this boord could not havt bttn mrchtd In a ltga gamt, In some sense, the puule needs to be solved before It Ciln be put In the acceptable form for the axioms. What we have here Is an Issue of language. There are certainly many questions one would like to as~ In, for example, English, for which natural language Is Inadequate. Imagine, If you will, the circumlocutions Involved In giving a written spelling test. The moral here Is an epistemological lncompiE'teness theorem; there will always be things that cannot be said In any system.

We have consider the axiom system In the light of other retrograde problems, and find that Is it effectively capable of expressing their solution. In particular, we have considered the problem in [4].* and find no difficulty in expressing its solution In our axlomatiution.

17. Summary

We have taken a difficult problem of retrograde analysis chess, deta iled a set of axioms for the rules of chess, and have shown that those axioms, together with a clever natural deduction system and the ability to simplify in a semantic model, are sufficient to produce a manageable derivation of the solution of a complicated problem. We have considered some of the conclusions that can be formed about formal knowledge representiltions from this work. Particularly we have explored, the nature of the objects of the chess world, such as state vectors, concrete ilnd abstract objects, and compound objects and the nlue of things such as semantic simplification, meta reasoning, modill reilsoning and Induction schema.

18. Acl< nowledgments

I would like to acknowledge the helpful advice provided by Drs. john McCarthy, Richard Weyhrauch and Terry Winograd in the course of pursuing this research.

I!J. References

• I Filman, Robert E., and R.W.Weyhrauch; An FOL Primer. Memo AIM-288, St~nford University, September 1976.
• 2 Fllman, Robert E.; The Jnttraction of Observation and !nference. PhD thesis, Computer Science Dept. Memo AIM­ ~27, Stanford University, March 1979.
• 3 Gardner, M utin; Mathematical Games In the Scientific Amrrican 202:!\ (May 19!\9).
• 4 Gardner, Mart in Mathematical Gamts in the Scientific American 228:5 (May 1973).
• 5 McCarthy, John; Tht Adt·ict Talttr. In M. Minsky, td. Srmantic Information Procrssln~. MIT Press, Cambridge, Ma~s . 1968.
• 6 McCarthy, John, and P.J. Hayes; Somt Philosophical Probltms from t/r( Stllndpoint of Artifidal lnt(/ligtnct. In Machine l.Dtelli~cnce 4, B. Meltter & D. Michie, eds. Edinburgh University Press, Edinburgh, 1969.
• 7 McCarthy, John; Epistemological Problems of Artificial lrtttlligence. In Proc. I!CAJ-77. MIT, Cambridge, Mass., August, 1977, pp I0:,\8.JOH.
• 8 McCarthy. John; (.{)nctpt valued functions. To appear In Machine lntelli~ence 9, D. Michie, ed.
• !J Weyhrauch, Richard W.; A User~ Manual for FOL. Memo AIM-235.1, Stanford University, 197 .
• 10 Weyhr~uch, R lchard W. 11nd Robert E Filman; M.tla. Reasonin~ and E:octcndcd Jnfcrcnc:c for AI (In fmpamtion'i. __ _

* Bl11ck kine on WQI, bishop on WQ5, rook on QN51 while bishop on WQR4. Where is the while king?