Some Notes on Reasoning


 by Sunil Vemuri

Propositional Logic

For a more detailed review of Propositional Logic, see Genesereth's CS 157 Course Notes.

Some stuff to know:

First Order Predicate Logic (FOPL)

For a more detailed review of FOPL, see Genesereth's CS 157 Course Notes.

Some stuff to know:

Generalized Modes Pones allows us to do a combination of Modes Pones, And Introduction and Universal elimination all in one step. Essentially it is an optimization that allows one to do several steps where we could only do one before. [Russell & Norvig, p. 269]

For example, if our database contained {P(A,x), Q(B), ForAll y P(A,C) & Q(y) => R(y)}
We can clearly see that R(B) is logically entailed. However, this would take several reasoning steps. With generalized Modes Ponens, we can do it in one reasoning step. Intuitively, this seems like a macro operation.

Soundness and Completeness

Soundness

Completeness

Godel's Completeness Theorem


Godel's completeness theorem basically states that for first order logic, any sentence that is entailed by another set of sentences can be proven from that set. Which is essentially what was stated above.

Godel's Incompleteness Theorem

Russell & Norvig give a one-page summary of the intuition of the proof on page 288 of their text.

Godel's Incompleteness theorem is a proof of the imposibility of proving. In Godel's completeness proof, we have completeness for first order logic in general. However, Godel proved that when we restrict our attention to the axiomatization of arithmetic (aka mathematical induction schema), this axiomatization is provably incomplete. This means there are true statements in mathematical induction schema that we cannot prove. The significance of this proof is that it shows that we can never prove all the theorems of mathematics within any given system of axioms. Mathematitions at the time believe otherwise, but Godel showed them otherwise.

Resolution

Introduction

Unification and Occurs Check




Resolution Strategies

Deletion Strategies

Unit Resolution

Input Resolution

Linear Resolution

Set of Support Resolution

Ordered Resolution

Directed Resolution

Prolog

Resolution with Equality


Without sentences involving the equality and inequality relations, resolution is refutation complete; i.e. given an unsatisfiable set of sentences, resolution is guaranteed to produce the empty clause (LFAI, page 85). Refutation completeness is based on Theorem 4.5 (page 89) in LFAI: "If a set S of clauses in unsatisfiable, then there is a resolution deduction of the empty clause from S."

Paramodulation and Demodulation are methods of handling equality while still allowing us to use resolution The other common ways are adding equality axioms to the database (transitivity, reflexivity, symmetry).

Paramodulaiton preserves refutation completeness but demodulation sacrifices refutation completeness. Demodulation is in fact a restricted form of paramodulation. Paramodulation can be comptationally expensive, so demodulation can be used in its place.

So, what is paramodulation and demodulation? One way to think about demodulation is performing a substitution. For example, if we have an equality u=v, then wherever u appears in a clause, we can replace it with v. Well, it's not that simple, but it's close. Using the example found in Genesereth's notes:
{P(F(F(A))),B), Q(B)}
{F(F(x))=G(x)}
From here, we can substitute G(x) wherever we find F(F(x)). F(F(x)) does not appear exactly, but we can perform a substitution x<-A on the equality clause and get F(F(A))=G(A). Now, wherever we find F(F(A)) in the first clause, we can replace it with G(A). The resulting clause is:
{P(G(A)), B), Q(B)}

There are a few restrictions on demodulation. First, the equality clause must be a unit clause. So, we cannot do demodulation if the clause was {F(F(x))=G(x), R(x)}. Second, when we unify the clauses, we can only perform the substitution on the unit equality clause.

Paramodulation relaxes these restrictions. Obviously demodulation is not complete because if we have any non-unit clauses with equality, we would not be able to prove some facts that are in fact entailed.

LFAI does not cover this in any detail, but Genesereth does cover it in his CS 157 Course Notes and it is coverd in Russell & Norvig p. 284.


Forward vs. Backward Reasoning



For logical reasoning tasks, one can either search forward from the inital state (forward chaining) or search backward from the goal state (backward chaining).

Forward Chaining
According to Rich and Knight, "Begin by building a tree of move sequences that might be solutions by starting iwth the initial configuration(s) at the root of the tree. Generate the next level of the tree by finding all the rules whose left sides match the root node and using their right sides to create the new configurations. Generate the next level by taking each node generated at the previous level and applying to it all of the rules whose left sides match it. Continue until a configuration that matches the goal state is generated."

Backward Chaining
According to Rich and Knight, "Begin building a tree of move sequences that might be solutions by starting with the goal configuration(s) at the root of the tree. Generate the next level of the tree by finding all the rules whose right sides match the root node. These are all the rules that, if only we could apply them, would generate the state we wanted. Use the left sides of the rules to generate the nodes at this second level of the tree. Generate the next level of the tree by taking each node at the previous level and finding all the rules whose right sides match it. Then using the corresponding left sides to generate the new nodes. Continue until a node that matches the initial state is generated. This method of reasoning backward from the desired final state is often called goal-directed reasoning ."

Which is better?
Rich and Knight cite four factors:
According to Winston, "Mycin is a backward chaining system, because physicians prefer to think about one hypothesis at a time. By sticking with questions that are relevant to a particular hypothetical conclusion, the questioning is guaranteed to remain relevant to that hypothesis." Mycin's uses a natural language question/answer dialog interface to get information to perform its reasoning. Another reason why Mycin used backward chaining (according to Rich & Knight): doctors are unwilling to accept the advice of a diagnostic program that cannot explain its reasoning to the doctor's satisfaction. Furthermore, in Mycin, rules can be augmented with probabilistic certainty factors to reflect the fact that some rules are more reliable than others.

Rich and Knight cite theorem proving as an application more suited to backward chaining because the branching factor is significantly greater going forward from the axioms than it is going backward from the theorems to the axioms. For example, Prolog uses backward chaining.

Rich and Knight cite symbolic integration as a domain suited for forward chaining for similar branching factor reasons. Symbolic integration involves the problem of taking a mathematical expression with integrals and finding an equivalent integral-free expression. Also, production systems are forward chaining.

Opportunistic Reasoning
There is also the notion of opportunistic reasoning where one chooses either backward or foward reasoning at the most "opportune time". According to Penny Nii, "Blackboard systems model of problem solving is a highly structured special case of opportunistic problem solving. In addition to opportunistic reasoning as a knowledge-application strategy, the blackboard model prescribes the organization of the domain knwledge and all the input and intermediate partial solutions needed to solve the problem."

References: Rich & Knight, Winston's AI Text, Penny Nii's Blackboard Systems paper.


Situation Calculus



Reasoning about action.
Frame Problem
Qualification Problem
Ramification Problem

Higer Order Logics

First order logics can quantify over objects in the universe of discourse. Second order logics can quantify over functions and relations in the unverse of discourse. (LFAI, p.20)

"The language of (full) second order logic is simply the language of first order logic augmented with second order variables , that is, variables ranging over relations and functions (of all arities)." [Leivant]

Some examples of a second order logic statments would be:

(x = y) <--> ForAll R R(x) <--> R(y)

(ForAll P) (Exists x) P(x) --> ForAll x P(x)

Here, we are quantifying over the relation R, whereas in first order logic, this would not be allowed. The consequence is we have a language which is more expressive than first order logic. The notion of satisfiability must be extended to handle quantified functions and predicates.

So, what are some neat things we can do with second order logic that we cannot do with first order. Leviant states a theorem: "The collection of finite structures is not first order definable, but is definable already by a single second order structure"

ForAll f (Inj(f) --> Surj(f)) where

Inj(f) is defined to be ForAll x,y (f(x) = f(y) --> x = y)

Surj(f) is defined to be ForAll u Exists v f(v) = u

Non-Monotonic Reasoning

Closed World Assumption
Inheritance Based Non-Logical Formalisms
Semantic Nets
Frames
Non-Monotonic Logics
Non-Monotonic Logic
Default Logic
Circumscription
Autoepistemc Logic
Sunil Vemuri <vemuri@cs.stanford.edu>