Logic

Lee Spector, lspector@hampshire.edu

Cognitive Science

Hampshire College

According to some, logic is the essence of intelligence.

For this reason, automating logical processes may be the key to automating intelligence.

Logic, and claims about its status as the foundation of all knowledge, have a long history.

There is a wide range of opinions in the AI community about the proper role of logic.

Aristotle's syllogisms

Barbara:

All men are mortal. (Major premiss)

Socrates is a man. (Minor premiss)

Therefore, Socrates is mortal. (Conclusion)

Celarent:

No fishes are rational.

All sharks are fishes.

Therefore, no sharks are rational.

Darii:

All men are rational.

Some animals are men.

Therefore, some animals are rational.

Ferio:

No Greeks are black.

Some men are Greeks.

Therefore, some men are not black.

These four syllogisms make up Aristotle's "first figure" (he also has a second and third).

Validity

All trout are mammals

All mammals have wings

Therefore, all trout have wings

Sentence variables

Connectives: not, and, or, implication, equivalence.

Symbols for boolean logic: +=OR, *=AND, '=NOT. Symbols vary.

There are 16 two-variable boolean functions.

You can make all 16 boolean functions out of just AND, OR, and NOT. In fact, you can get by with just AND and NOT. Because of this {*,'} is called a "complete base." {+,'} is also a complete base. The NAND function all by itself is a complete base.

Truth tables

A    B    A and B
F    F       F
F    T       F
T    F       F
T    T       T

A    B    A nand B
F    F       T
F    T       T
T    F       T
T    T       F

A    B     A or B
F    F       F
F    T       T
T    F       T
T    T       T

A    B     A = B
F    F       T
F    T       F
T    F       F
T    T       T

A    not A
F      T
F      F

A    B     A -> B
F    F       T
F    T       T
T    F       F
T    T       T

Tautologies -> truth tables all true.

Contradictions -> truth tables all false.

We can use logic notation to form complex logical expressions--we can also use a graphical notation to draw complex logical expressions.

(A & B) v ~((C & D) & (E v F))

LogicSim 2.2

Proofs via the Truth Table method grow exponentially.

An alternative proof technique uses rules of inference:

Modus Ponens: P ... Q, P, therefore Q

Modus Tollens: P ... Q, ~Q, therefore ~P

Hypothetical Syllogism: P ... Q, Q ... R, therefore P ... R

A proof system that applies rules of inference to an initial set of premises can be thought of as a machine for cranking out theorems: truths in the top, proven new truths out the bottom...

Sound system: rules of inference preserve truth.

Complete system: all truths can be proven.

Gödel's incompleteness theorem: systems that are at least strong enough to prove certain relatively simple arithmetical truths cannot be both sound and complete.

A more efficient proof algorithm for propositional logic is Wang's algorithm.

Wang's algorithm: VALID?

Start with a single "sequent" with all premises on the left and the desired conclusion on the right:

for example, P...Q, Q...R, ~R fi_s ~P

Loop:

If some top-level formula occurs on both the left and right sides then return VALID.

 

If all formulas in the sequent are just symbols and no symbol occurs on both sides return INVALID.

 

If a formula anywhere is of the form X...Y then replace it with ~XvY and call VALID? recursively.

 

If a top level formula has the form ~X then delete it, add X on the other side of the arrow, and call VALID? recursively.

 

If a top level formula on the left has the form X&Y or one on the right has the form XvY then replace the connective with a comma and call VALID? recursively.

 

If a top level formula on the left has the form XvY then make two recursive calls, one with X substituted for the XvY, and one with Y substituted for XvY. Return the result of AND applied to the results.

 

If a top level formula on the right has the form X&Y then make two recursive calls, one with X substituted for the X&Y, and one with Y substituted for X&Y. Return the result of AND applied to the results.

 

Tanimoto provides an implementation of Wang's algorithm. Here is the most important function:

;;; VALID is the main recursive workhorse that verifies
;;; the propositional logic "theorems" with Wang's rules.
;;; Pattern-matching results are passed back as and stored
;;; locally as the value of B -- the "bindings".
;;; Arguments L and R are the left and right sides of a sequent.
(defun valid (l r)
  "Returns T if the conjunction of the formulas in L implies
   any of the formulas in R."
  (let (b)
    (cond
      ; Test for axiom:
      ((intersection l r) t)
      ; NOT on the left:
      ((setf b (match '((* x) (not-wff y) (* z)) l))
       (valid (append (val 'x b) (val 'z b))
              (append r (rest (val 'y b))) ) )
      ; NOT on the right:
      ((setf b (match '((* x) (not-wff y) (* z)) r))
       (valid (append l (rest (val 'y b)))
              (append (val 'x b) (val 'z b)) ) )
      ; OR on the right:
      ((setf b (match '((* x) (or-wff y) (* z)) r))
       (valid l 
              (append (val 'x b) 
                      (list (first (val 'y b)))
                      (rest (rest (val 'y b)))
                      (val 'z b) ) ) )
      ; AND on the left:
      ((setf b (match '((* x) (and-wff y) (* z)) l))
       (valid (append (val 'x b)
                      (list (first (val 'y b)))
                      (rest (rest (val 'y b)))
                      (val 'z b) )
              r) )
      ; OR on the left:
      ((setf b (match '((* x) (or-wff y) (* z)) l))
       (and (valid (append (val 'x b)
                           (list (first (val 'y b)))
                           (val 'z b) )
                   r)
            (valid (append (val 'x b)
                           (rest (rest (val 'y b)))
                           (val 'z b) )
                   r) ) )
      ; AND on the right:
      ((setf b (match '((* x) (and-wff y) (* z)) r))
       (and (valid l
                   (append (val 'x b)
                           (list (first (val 'y b)))
                           (val 'z b) ) )
            (valid l
                   (append (val 'x b)
                           (rest (rest (val 'y b)))
                           (val 'z b) ) ) ) ) ) ) )


? (prover)

Please enter proposition or HELP or RETURN.

(a or (not a)) is valid.

Please enter proposition or HELP or RETURN.

((a or (not a)) and (b or (not b))) is valid.

Please enter proposition or HELP or RETURN.

(a and (not a)) is NOT valid.

Please enter proposition or HELP or RETURN.

((a implies b) and (b implies (not a))) is NOT valid.

Please enter proposition or HELP or RETURN.

help

Here's an example: ((a and (not b)) implies a)

Please enter proposition or HELP or RETURN.

((a and (not b)) implies a) is valid.

Please enter proposition or HELP or RETURN.

((a and (not b)) implies b) is NOT valid.

Please enter proposition or HELP or RETURN.

return

NIL

?

Deviant logics

Future contingents: Aristotle: There will be a ship battle tomorrow

Quantum Logics

Modal logics

Logics of vagueness

Fuzzy logics

Example: Lukasiewicz's 3-valued system

A    B    A and B
F    F       F
F    T       F
F    I       F
I    F       F
T    F       F
T    T       T
T    I       I
I    T       I
T    T       T

A    not A
F      T
F      F
I      I

The predicate calculus

predicates

blue(x)

mortal(x)

on(x,y)

member(x,y)

oddp(x)

universal and existential quantifiers

ForAll(m)(mouse(m))

Exists(c)(cat(c))

ForAll(m)((mouse(m) & on(m, DOORSTEP)) -> Exists(cat(c) & killed (c, m)))

Next time: clause form, unification, resolution, Prolog