CSE 150 Lecture Notes, November 29, 2004

CSE150 LECTURE NOTES

November 29, 2004

ANNOUNCEMENTS

Doug has persuaded me to reduce the scope of Assignment 4. I hope you have started work on this already. Using Otter is not easy!

Remember that the final exam is coming in just one week, on Monday December 6.

A SOLUTION TO THE FRAME PROBLEM

One solution is as follows. We use three basic predicates: "holds", "causes", and "cancels", and we formalize some commonsense knowledge:

``A fluent holds in the state resulting from an action if and only if the action `causes' the fluent, or the fluent held before the action, and the action does not `cancel' it.''

We write this general knowledge about the three predicates "holds", "causes", and "cancels" in our ontology as

forall a,s,p holds(p,do(s,a)) <-> causes(a,s,p) \/
[ holds(p,s) & ~cancels(a,s,p) ]

Only two more axioms are needed to describe the Yale shooting world:

forall a,s,p causes(a,s,p)    <->
       [ a=load & p=loaded] \/
       [ a=shoot & p=dead & holds(loaded,s)]
forall a,s,p cancels(a,s,p)    <->
       [ a=shoot & p=alive & holds(loaded,s)] \/
       [ a=shoot & p=loaded & holds(loaded,s)]

Some notes about this solution to the frame problem:

For each positive or negative effect of each action, we add one line to the causes or cancels axiom.
The fluent wait is axiomatized without mentioning it explicitly, because it has no effects.
Causing a fluent dominates canceling the same fluent.
An action whose preconditions are not satisfied can be performed, but it has no effect.

THE "ENTAILS" NOTATION

Suppose we write T |= A. The symbol |= is pronounced "entails." This means that in every universe where every axiom in T is true, the sentence A is also true. (In lecture we used t he notation KB for "knowledge base" instead of T for "theory.") For example:

T & holds(loaded,s_0) |= cancels(shoot,s_0,alive)

Otter uses proof-by-contradiction, so with Otter we would have

T & holds(loaded,s_0) & -cancels(shoot,s_0,alive) |= contradiction

REASONING FORWARDS AND BACKWARDS IN TIME

Let T be the set of three axioms stated above. The original shooting problem is solvable:

T & holds(alive,s_0) |= holds(dead,do(do(do(s_0,load),wait),shoot)).

Suppose the turkey is known to be alive originally, but a shot was heard and the turkey was seen dead some time later. Whodunit? This murder mystery is also solvable:

T & holds(alive,s_0) & ~holds(alive,do(do(s_0,shoot),wait))
|= holds(loaded,s_0) & cancels(shoot,s_0,alive)

Intuitively, the frame axiom says that miracles never happen: if a fluent holds, then it must have just been caused by some action, or else it must have held immediately previously, and not been canceled.

PLANNING PROBLEMS

Given information about the initial state, the planning task is to discover a sequence of actions such that certain fluents hold in the final state. Example: find P such that

T & holds(alive,s_0) |= holds(dead,P).

The answer is P = do(do(do(s_0,load),wait),shoot)

Solving a planning problem requires a logical reasoning system (i.e. a knowledge base manager or inference engine) that can return existential witnesses in addition to saying (yes, no, or unknown) whether or not a certain sentence is entailed by a given knowledge base.

Unfortunately, doing planning by general-purpose logical reasoning is just not efficient computationally. The most successful planners today operate by translating a first-order knowledge base into propositional 3SAT clauses, then running a local search algorithm like WalkSat.

COMPLETENESS AND SEMI-DECIDABILITY

Suppose we write T |- A. The symbol |- is pronounced "proves." This means that the sentence A can be proved by a theorem-proving algorithm (for example Otter) starting from the sentences in T.

Ideally, we want to have T |- A if and only if T |= A. However this "if and only if" is not achievable.

Definition: The proof algorithm |- is complete if whenever KB |= A then KB |- A in finite time. Here |= means logical entailment, which is a semantic notion, while |- means provability, which is a syntactic, i.e. algorithmic notion. Completeness says that if A is true, then it can be proved eventually.

Note that this definition of "complete" says nothing about what happens with |- when KB |/= A, i.e. KB does not entail A. Therefore, using the name "complete" for this definition is slightly confusing and a better name would be "semi-complete." If we use the name "semi-complete" for the concept above, then "complete" would mean "KB |- A if and only if KB |= A, and |- always terminates."

Given KB and A, it may be the case that KB does not entail A, and also that KB does not entail ~A. Completeness says nothing about this case, where KB leaves the truth value of A unsettled.

Definition: The entailment relation |= is semi-decidable if a complete proof algorithm exists for it. Entailment |= is decidable if a proof algorithm exists that is complete and also always terminates in finite time.

Gödel's completeness theorem: First-order logic entailment |= is semi-decidable. In iother words, there exists a theorem-proving algorithm |- that is sound and complete (for the definitin of complete immediately above).

Gödel's incompleteness theorem (alternative statement): First-order logic entailment |= is not decidable.