CSE 150 Lecture Notes, February 5, 2003

CSE150 LECTURE NOTES

February 5, 2003

ANNOUNCEMENTS

The deadline for the current project is pushed out to Friday next week, in section at 2pm. (The reason is that many people have compiler project deadlines early next week.)

There is a research talk right after lecture today about local search methods for solving 3SAT problems. Go to APM room 4218.

AXIOMATIZING KNOWLEDGE

Our topic is how to state knowledge explicitly, and soon, how to draw conclusions from knowledge. In AI this field of research is called knowledge representation and reasoning (KRR).

An ontology is the collection of basic concepts that we choose to use to describe our intended interpretation. Formally, it is our particular first-order vocabulary of constant-symbols, function-symbols, and predicate-symbols.

When you write down knowledge formally, the real knowledge is in the interrelationships between predicates and functions, not in the names of the predicates and functions, because constant-symbols, function-symbols, and predicate-symbols are uninterpreted.

It is very important for you to understand what the following statement means: Constant, function, and predicate symbols are uninterpreted. It means that, for example, daughter(Mary) designates a semantic entity that, as far as we know, can be the same as or different from every other semantic entity.

Typically, you have an intended interpretation in mind. You write down as many axioms as possible that are useful. An axiom is useful if it is true but not redundant, that is true in the intended interpretation but false in some unintended interpretation, so that it excludes this undesired model of the other axioms.

THE PEANO AXIOMS FOR THE NATURAL NUMBERS

If you write down too few axioms for any domain, then your knowledge base will have incorrect, unintended models. Typically, it is impossible to eliminate all undesired models, because of the lack of expressiveness of FOL.

Consider the Peano axioms for the natural numbers:

int(0)
forall x int(x) -> int(succ(x))

We would like these axioms to have only one model, namely the natural numbers, but in fact the axioms also have nonstandard models. We can add additional axioms, e.g.

forall x int(x) <-> x = 0 \/ exists y x = succ(y)

but Godel's incompleteness theorem says that we will never succeed in writing down a collection of FOL axioms that pin down the natural numbers fully.

REPRESENTING HOW THE WORLD CHANGES

The traditional ontology for reasoning about action is called the situation calculus and is due to John McCarthy of Stanford. It involves three basic categories:

a "state" is a snapshot of the world,
a "fluent" is a changing relationship between objects, and
an "action" is an event that changes one state into another.

States, fluents, and actions can be represented by FOL terms built from constant-symbols and function-symbols:

a and b can be constants naming two blocks,
s_0 can be the name of the beginning state of the world
stack(a,b) can name the action of placing a on b,
do(s_0,stack(a,b)) can name the state resulting from doing this action in the initial state s_0.

Note that do(s_0,a) where a is an action is very similar to succ(0) in Peano arithmetic.

FOL is a formal language in the same way that Java, C, etc. are formal languages. Intuitively, FOL should have types also. For example, a and b are two constant-symbols that have the same type, while s_0 is a constant symbol that has a different type. Unfortunately, FOL does not let us specify types. Therefore, it is very easy to make type mistakes in FOL.

Fluents cannot be represented as predicates because they are not simply true or false. Rather, they are true in some states and false in others.

We use a predicate named holds to connect fluents with states. For example:

holds( ontopof(a,b), do(s_0, stack(a,b)) ).

SYNTACTIC, SEMANTIC, AND TYPE ERRORS IN FIRST-ORDER LOGIC

Why do we have a fluent obstructed(b) ? Why not just use ~clear(b)? Answer: it is a syntax error to apply the negation connective ~ to anything that is not a sentence. Syntactically, clear is a function-symbol, and clear(b) is a term, not a sentence.

We can write an axiom sentence such as forall s forall x holds(obstructed(x),s) <-> ~ holds(clear(x),s). In this axiom holds(clear(x),s) is syntactically a sentence so applying negation to it is well-formed.

The error of writing ~clear(b) in FOL is similar to the error of writing x++ in C where x is a floating point variable. The meaning may be intuitively clear, but formally speaking, the syntax is not allowed.

The syntax of FOL does not protect us from two other error categories: (1) semantic errors and (2) type errors.

A semantic error is a sentence that is not true in the intended interpretation. For example, given the desired meaning of dead and alive, this sentence is a semantic error: exists x holds(clear(x),s) & holds(obstructed(x),s).
A type error is a sentence using constant-symbols or function-symbols in an incompatible way. The following sentence is a type error:forall x holds(clear(x),unstack(x)), because unstack(x) is an action, not a state.