First order logic allows the use of sentences that contain variables. So that rather than the proposition

Socrates is a manone can have sentences of the form

X is a manwhere X is a variable.

To work with these things we need to enrich the grammar of propositional logic with two extra notions.

- Terms
- terms are used to refer to objects as mother_of(Mary)
- Quantifiers
- These are used to express properties of collections of objects.

We provide the grammar in a slightly less formal presentation than that in AIMA. As before the goal is to describe the syntactically allowable sentences.

- A sentence is one of
- An atomic sentence
- Sentence Connective Sentence
- Quantifier Variable Sentence
- ~ Sentence
- (Sentence)

- An atomic sentence is one of
- Predication(Term, ... ) (A function whose range is {true, false})
- Term = Term

- A term is one of
- Function(Term, ...)
- Constant,
- Variable

- A connective is one of = > , /\, \/, < = >
- A quantifier is one of E (there exists, actually backwards E ) or A ( for all, actually upside down A)
- The constants are drawn from some set of constants , (a , b, c, John, etc)
- The variables are drwn from som eset of variables, (x,y,z, etc)
- the predicates are drawn from some set of predicate names ( next_to, has_color, etc)
- The function names are drawn from some set of function names (mother, sizeof etc)

The notion of a model for a set of sentences in first order logic has a natural definition. At the risk of some oversimplification there is a universe U, which contains all the objects referred to by the constans and on which all the functions and predicates are defined. A sentence is satisfiable if the varaibles that appear in it can be chosen from the Universe so as to make it true. This leaves only quantification. Here is a quick semantics for the quantifiers.

- (Ex) f(x) is true iff f(x) is satisfiable.
- (Ax) f(x) is true iff ~ (Ex) (~f(x)) is true.

First order logic is much harder than propositional logic. Proof procedures are harder to use because there are so many more choices, we will not pursue the matter here. Some ideas on proof procedures for FOL are described in the page on inference.

If agents are to be able to work sucessfully in the real world they need to be able to reason about the consequences of their actions. Note that reflex agents do not do this, making them unsuitable for applications in which the world changes. On the other hand it is easy to see how a reflex agent's behaviour is expressible in terms of FOL. Thus:

forall s,b,u,c,t ( Precept([s,b,Glitter, u,c], t) => Action(Grab, t)encodes the desirablity of grabbing the gold when you see glitter.

Unfortunately reflex agents will always respond to a given percept set in the same way. So that they will end never be able to make a different choice from their first one. This is where some reasoning ability is needed. If we made the reflex agent inot a table driven agent that reacted based upon the sequence of past percepts then presumably we could choose differently on reencountering the same percept at the same place. As before it is unfeasible to store all this information. Fortunately it is enough to be able to keep track of the present state.

Michael Leyton in his book, "Symmetry, Causality, Mind" makes the interesting observation that asymmetry is history so that as T.S. Eliot says

"Time present and time pastOne way in which one can keep track of the present state is through the situational calculus.

Are both perhaps present in time future,

Last Changed: 19 October 1995