Logic

• Advantages:

  1. consistency and precision

  2. completeness

  3. easily mechanized

  4. easy to write (logic programming) and understand

  5. natural for some problem representation

  6. modularity

• Disadvantages:

  1. not suitable for representing general knowledge (commonsense knowledge). No uncertainty.

  2. no heuristics, combinatorial explosion

  3. do not simulate cognitive process

  4. formal structure of logic constrains the reasoning process.

Propositional Calculus

Def: A proposition is a declarative sentence that must either be true or false but not both.

• not all sentences are declarative sentences.
  e.g. (a) Pass me the butter
  (b) Has flight 201 from New York arrived?

• not all declarative sentences ar propositions.
  e.g. This sentence is false (Russell paradox)

Propositional Calculus Axiom:

Every proposition is either true or false (but not both).

A well-formed formula (wff) is defined recursively:

1. All propositional variables and the constants TRUE and FALSE are wff's.

2. if a, b are wff;s, then the followings are wff's:
   

3. Nothing else is a wff.

A tautology is a wff that evaluates to true for all possible truth assignments to its variables, e.g.

A contradiction is a wff that evaluates to false for all possible truth assignments to its variables, e.g.

A wff that is not a contradiction is said to be satisfiable.

A literal is either a propositional variable or its complement.
(e.g. )

A wff is in conjunctive normal form (CNF) iff it is the conjunction of clauses each of which is the disjunction of literals.

e.g.

A wff is in disjunctive normal form (DNF) iff it is the disjunction of clauses each of which is the conjunction of literals.

e.g. 

Resolution Principle for Propositional Logic

Modus Ponen: or

• Looks like the the p and ~p can cancel each other.
  
  

• More formally, if we have clauses of disjunction of literals, C₁ and C₂:
  where P, Q are clauses of disjunction of literals.

Thm Given two clauses C₁, C₂, a resolvent R (º PVQ) of C₁ and C₂ is a logical consequence of C₁ and C₂.

Pf: Let C₁ = S V P
C₂ = ~S V Q
R = P V Q

case 1: if S=true, then Q=true => R=true

case 2: if S=false, then P=true => R=true

i.e. C₁ ^ C₂ => R

Given a set S of clauses, a resolution of C from S is a finite sequence C₁, ..., C_k of clauses such that each C_i is either a clause in S or a resolvent of clauses preceding C_i and C_k = C.

Prove by Refutation

' -> contradiction (empty clause)

A set of clauses is unsatisfiable (inconsistent) iff there is a resolution deduction of the empty clause ' from S.

i.e. "Contradiction is a logical consequence of S".

S => F º T => ~S, hence ~S is true, or S is false.

Example:

1. ~p V q

2. ~q

3. p

4. [From (1) & (2)] ~p

5. [From (3) & (4)] '

Predicate Calculus

Consider the premises:

P1: Nothing intelligible puzzles me

P2: Logic puzzles me

Conclusion:

C: Logic is unintelligible

The validity of the conclusion from premises P1 and P2 cannot be established in propositional logic. Proposition with variable is needed.

A Predicate P(x₁, x₂, ..., x_n) n>0 is a mapping from x₁, x₂, ... x_n to the value true or false. n is the degree of the predicate.

e.g.

In predicate calculus, besides predicates and variables, the use of quantifiers allow flexible representation.

Quantifiers

Universal quantifiers

Existential quantifiers

The scope of a quantifier is the wff to which it applies.

e.g.

An occurrence of a predicate variable x is free iff that ocurrence is not within the scope of a quantifier that quantifies x.

An occurrence of a predicate variable x is bounded iff it is not free.

wff in FOL (First Order Logic)

1. All propositional variables, predicates and the constants true and false are FOL wffs. A predicate with some of its parameters set to constants (e.g. P(a)) is also a FOL wff.
   

2. If a and b are FOL wffs, then the following are also FOL wffs
   provided that all occurrences of the same predicate name have the same number of parameters.

3. are FOL wffs whenever a is a FOL wff and x is not bounded in a.

4. Nothing else is a first order logic wff.

Clausal form

A clause is an expression of the form:

or,

or,

which is a disjunction of literals.

Hence clausal form is in CNF such that all free variables are universally bound.

Representation in Predicate Calculus

Example 1

P1: No professors are ignorant

P2: All ignorant people are vain

C: Some vain persons are not professors

U (Universe of discourse) = set of all people
P(x) : x is a professor

V(x) : x is vain

I(x) : x is ignorant

Example 2

P1: All philosophers are logical

P2: An illogical person is always obstinate

C: Some obstinate person are not philosophers

U (universe of discourse) = set of all people

P(x) : x is a philosopher

Q(x) : x is logical

R(x) : x is obstinate

Prenex Normal Form

A wff in the FOL is in prenex normal form (PNF) iff it is of the form:

Q₁x₁Q₂x_2. ... Q_kx_k a

where Q_i's are quantifiers (" or $), the x_i's are distinct predicate parameters and a is an FOL wff containing no quantifiers.

For every FOL wff not in PNF, there exist an equivalent FOL PNF wff.

FOL equivalences:

Transformation to PNF

1. Eliminate implications :

2. Move negation down to atomic formulae by using de Morgan law and (7), (8).

3. Rename bound variables if necessary (Rule 1 and 2)

4. Use rules 3-12 to move quantifiers to the left

Examples:

Step1: Eliminate implication

Step2: Move negation down to atomic formulae

Step3: Rename bound variable

Step4: Move quantifier to left

Apply rule 5, 6:

Apply rule 3, 4:

Skolem Standard Form

A FOL wff is in skolem standard form if

1. It is in PNF

2. All quantifiers are universal quantifier

3. the clause is in CNF

Transformation to Skolem Standard Form

1. Change to PNF

2. Change clause to CNF

3. Eliminate existential quantifier, probably introducing Skolem functions.

e.g.

• the value of y may depend on that of x, i.e. different x may have different y.

• Introduce y as a function of x, say f(x)
  Skolemisation
  
  If $y is not within the scope of any universal quantifier, then just replace variable with a constant.
  e.g. $y P(y) is replaced by P(a).

Remark: The result of skolemisation is not equivalent to the original wff. Rather, it is a logical consequence of it.

Example

Step2: change to CNF

Step3: Skolemisation

Let u=Support(x)

Clausal Form

A clausal form can be obtained by purging all universal quantifiers, by renaming variables and eliminating conjunctions.

The process of PNF and skolemisation can be combined into one process (and rearranging the procedures):

1. eliminate implications

2. move negation down to the atomic formulae

3. purge existential quantifier (introduce skolem function)

4. rename variables, if necessary

5. move universal quantifiers to the left

6. move the disjunction down to the literal (to form CNF)

7. eliminate conjunction

8. rename variables, if necessary

9. purge universal quantifier.

Substitution and Unification

Substitution is substituting variables in an expression by some values (or expression)

e.g. {a/x, b/y} means x is substituted by a, and y is substituted by b.

e.g.

Unification is the process of finding a substitution such that when applied to expressions E₁ and E₂, they will produce the same result.

i.e. E₁ s=E₂ s, s is the subsitution.

The expression E₁ and E₂ is said to be unifiable.

Intuitively, (not rigorous definition), the most general unifier (mgu) is the substitution which yields the most general result, i.e. use as little substitutions as possible.

e.g. E₁=x, E₂=g

then s={a/x, a/y} is a unifier, since

E₁ s=a=E₂ s

However, this is not most general. Actually,

mgu={y/x}, or {x/y}

Theorem Proving by Resolution Refutation

• given a set of axioms

• Is a logic expression a logical consequence of the axioms?

Observation:

If axioms are S₁, ..., S_n and theorem to prove is T, then, if T is a theorem,

Hence,

Procedure:

1. negate the theorem to be proved and add the result to the list of axioms

2. put the axioms in clausal form

3. until the empty clause ' is produced or there is no resolvable pair of clauses, find resolvable clauses (probably with a unifier), resolve them, and add the result to the list of clauses.

4. If the empty clauses is produced, then the theorem is TRUE. If there are no resolvable clauses, the theorem is FALSE.

Example: Given that

Prove that

• (3), (4) & ~(5) are already in clausal form.

Step1: change (1), (2) to clausal form:

1. eliminate implications:
   

2. move negation down to atomic formula [OK]

3. purge existential quantifier [OK]

4. rename variables [OK]

5. move universal quantifier to the left [OK]

6. move disjunction down to literal [OK]

7. eliminate conjunction [OK]

8. rename variables
   

9. purge universal quantifiers

Step 2: Resolution Refutation

Resolve (2) & (5): Unifier={Table/u, B/z}

Resolve (1) & (6): Unifier={Table/y, v/x}

Resolve (1) & (7): Unifier={v/y, B/x}

Resolve (4) & (8):

Resolve (3) & (9):

'

Remark:

1. satisfiability problem is NP-complete. Resolution refutation is in effect solving the satisfiability problem. Hence it essentially searches the solution space and is subject to combinatorial explosion problem (exponential time required).

2. resolution do not guarantee termination, unless there is a proof. (semi-decidable problem).

Example1 (Professor example)

In clausal form:

Resolve (1), (3):

Resolve (2), (4):

cannot proceed.

Problem: we do not know whether there is any ignorant people. If by adding I(a) {$x I(x)} the theorem can be proved.

Example2 (Philosopher example)

In clausal form:

Resolve (1), (3):

Resolve (2), (4):

cannot proceed.

Improving speed of resolution

• subject to combinatorial explosion problem

• subject to a version of halting problem: no guarantee to terminate unless there actually is a proof (semi-decidable).

Strategies:

1. Unit Preference Strategy

   • give preference to resolution involving the clause with the smallest number of literals.

2. Set-of-support Strategy

   • allows only resolutions involving the negated theorem or new clauses derives (directly or indirectly) from it.

3. Breadth-first Strategy

   • first resolve all possible pairs of the initial clauses, then resolves all possible pairs of the resulting set together with the initial set, level by level.

All these strategies are complete, i.e. guarantee to find a proof if there is one.

Horn Clauses

Horn clauses are clauses that contain at most one "positive" literal.

e.g.

or,

Resolution of Horn clauses are simpler than general clauses.

e.g.

• during resolution, given the conclusion of one Horn clause, find in the RHS of another clauses whether a term is unifiable with it, e.g. b₁ in the above example. Then the 2 horn clauses are resolvable and the resolvent is obtained by substituting the RHS of (1) into (2).

Monotonic and non-Monotonic Logic

• when we add a new axiom, the theorem provable before adding the axiom will still be provable under the new set of axioms û monotonic.

• traditional logic is monotonic

• Some natural problem is not monotonic û non-monotonic logic.

• e.g. All birds can fly (1)
  Penguin is a bird (2)

  Then you may conclude Penguin can fly. When you add Penguin cannot fly, then that theorem cannot be proved anymore.

Weakness of Theorem Proving

1. NP-completeness û Exponential time.

2. difficult to formulate problem in logic form. Some problem may require second order logic.

3. logic may be weak to represent some kind of knowledge.
   e.g. time variation 0 temporal logic.

4. separation of representation and processing (declarative)

   The difficulty with most AI system lies in the heuristic part of the system, ie. in determining how to use the facts stored in the systems's data structure, not in deciding how to store them.

Advantage of Logic

• logic is precise

• logic is flexible (no commitment to the kinds of process that will make deductions, as logic is declarative)

• logic is modular.