FORMAL REASONING GROUP

http://www-formal.stanford.edu/

John McCarthy (logical AI +) Carolyn Talcott (math of programs)

Tom Costello (logical AI +)

Saša Buvač (formal theories of context) (finishing)

Eyal Amir( object oriented logic) Aarati Parmar (logic of action and knowledge)

AFOSR, DARPA HPKB

ROADS TO HUMAN LEVEL AI?

biological—imitate human, e.g. neural nets, should work eventually engineering—solve problems the world presents, presently ahead

direct programming, e.g. genetic algorithms, presently ahead

use logic, loftier objective

The logic approach is the most awkward—except for all the others that have been tried.

Logic in AI

Features of the logic approach to AI.

• Represent information by sentences in a logical language, e.g. first order logic, second order logic, modal logic.

• Auxiliary information in tables, programs, states, etc. is described by logical sentences.

• Inference is logical inference—deduction supplemented by some form of nonmonotonic inference.

• Action takes place when the system infers that it should do the action.

• Observation of the environment results in sentences in memory.

Topics, methods and problems of logical AI

• deduction, nonmonotonic reasoning, theories of action, problem solving, reifying concepts, reifying contexts, approximate objects, elaboration tolerance

• Elaboration tolerance (educate without brain surgery)

Elaboration Tolerance

Three missionaries and three cannibals come to a river and find a boat that holds two. If the cannibals ever outnumber the missionaries on either bank, the missionaries will be eaten.

How shall they cross?

\begin{matrix}331 → 310 → 321 → 300 → 311 → 110 → 221 → \\ 020 → 031 → 010 → 021 → 000. \end{matrix}

That’s the solution. What more is there to say?

ENGLISH LANGUAGE ELABORATIONS (1)

• The boat is a rowboat.

• The missionaries and cannibals have hats, all different.

• Four missionaries and four cannibals • There is an oar on each bank. One person can cross

in the boat with just one oar, but two oars are needed if the boat is to carry two people.

• The boat leaks and must be bailed concurrently with rowing.

• The boat may suffer damage and have to be taken back to the left bank for repair.

ENGLISH LANGUAGE ELABORATIONS (2)

• There is a bridge.

• There is an island.

• Only one missionary and one cannibal can row.

• The missionaries can’t row.

• If the biggest cannibal is isolated with the smallest missionary, the latter will be eaten.

• The biggest cannibal cannot fit in the boat with another person.

ENGLISH LANGUAGE ELABORATIONS (3)

• One of the missionaries is Jesus Christ. Four can cross. Here we are using cultural literacy. However, a human will not have had to have read Mark 6: 48–49 to have heard of Jesus walking on water.

• Three missionaries alone with a cannibal can convert him into a missionary.

• The probability is 1/10 that a cannibal alone in a boat will steal it.

• There are two (or N) sets of missionaries and cannibals too far apart along the river to interact.

KINDS OF ELABORATION (1)

• irrelevant actors, actions and objects • adding preconditions, actions and objects • changing a parameter

• making an entity situation dependent • specialization • generalization

KINDS OF ELABORATION (2)

• going into detail

• missionaries and cannibals as actors • simple parallel actions

• full concurrency • events other than actions • comparing different situations AD HOC AMAREL AXIOMS FOR BASIC MCP (1)

States = Z4 × Z4 × Z2

(∀state)(Ok(state) ≡

Ok1(P 1(state), P 2(state)) ∧Ok1(3 − P 1(state), 3 − P 2(state)))

(∀m c)(Ok1(m, c) ≡ m ∈ Z4 ∧ c ∈ Z4 ∧(m = 0 ∨ m ≥ c))

Moves = {(1, 0), (2, 0), (0, 1), (0, 2), (1, 1)} (∀move state) (Result(move, state) = Mkstate(P 1(state) − (2P 3(state) − 1)P 1(move), P 2(state) − (2P 3(state) − 1)P 2(move), 1 − P 3(state)))

AD HOC AMAREL AXIOMS FOR BASIC MCP (2)

\begin{matrix}(∀s1 s2)(Step(s1, s2) ≡ \\ (∃move)(s2 = Result(move, s1) ∧ Ok(s2))) \end{matrix}

Attainable1 = T ransitive-closure(Step)

Attainable(s) ≡ s = (3, 3, 1) ∨ Attainable1((3, 3, 1), s) From these we can prove

attainable((0, 0, 0)).

SIMPLE SITUATION CALCULUS MCP (1)

¬Ab(Aspect1(group, b1, b2, s)) → V alue(Inhabitants(b1), Result(Cross(group, b1, b2), s))

= V alue(Inhabitants(b1), s) \ group ∧ V alue(Inhabitants(b2), Result(Cross(group, b1, b2), s))

= V alue(Inhabitants(b2), s) ∪ group,

(1)

where \ denotes the difference of sets.

\begin{matrix}(∃x ∈ group)(¬Holds(At(x, b1), s)) \\ → Ab(Aspect1(group, b1, b2, s)). \end{matrix}

\begin{matrix}Holds(Bad(bank), s) \\ ≡ \\ 0 < \\ Card(\{x|x ∈ Missionaries ∧ Holds(At(x, bank), s)\}) \\ < Card(\{x|x ∈ Cannibals ∧ Holds(At(x, bank), s)\}) \end{matrix} (2)

Holds(Bad, s) ≡ (∃bank)Holds(Bad(bank), s).  (3)

\begin{matrix}¬(∃x)(x ∈ group ∧ Rower(x)) \\ → Ab(Aspect1(group, b1, b2, s)). \end{matrix}  (4)

The oar-on-each-bank elaboration is expressed by conjoining

Card(group) >
Card({x|Oar(x) ∧ Holds(In(x, Boat), s)})
→ Ab(Aspect1(group, b1, b2, s))

CONCLUSION

• Human level AI is hard.

• Logical AI is progressing.

• Too many researchers have too limited objectives.

• Machine learning has been fixated on classification via unary predicates.

• Maybe you should find your own approach—in logic or elsewhere.