Inference in Propositional Calculus

Non-SFS Reality Check

  1. If you can't do this, study a bit.
  2. If P implies Q and Q implies P then either P or Q is true.

    Put this statement into propositional calculus notation and prove or disprove it by a truth table. If the statement is false, what values of P and Q make it false?


Inference is useful because:

Technical Terms: Soundness and Completeness

Soundness: inference proves only true things.

Completeness: all true things can be proved.

More formally,
KB |=i α means that sentence α can be derived from KB by a procedure i.

Soundness: i is sound if:
      whenever KB |=i α, it is also true that KB |= α.

Completeness: i is complete if:
      whenever KB |= α, it is also true that KB |=i α.

Both propositional and first-order logics have sound, complete proof systems (inference rules and axioms). Thus a procedure can answer any question whose answer logically follows from the KB.

There are many known complete proof systems for PC: sets of simple rules for rewriting PC sentences into equivalent ones, that are complete. One has seven rules, ranging from the simple, like
(A ∧ A) ⇔ A and
(A ∨ B) ⇔ (B ∨ A) to the perhaps less obvious:
(B ⇒ C) ⇒ ((A ∨ B) ⇒ (A ∨ C)) .

We'll see some sample logical inference rules and identities below, but the only complete inference system we'll seriously consider is based on one inference rule: resolution.

Technical Terms: Validity and Satisfiability

Inference Process

For us, inference is rewriting sentences or generating new sentences by appying logical identities or rules of inference. For example, we may start with a KB of facts and rules and a sentence to prove, and inference combines the sentences of the KB to preserve truth and ultimately to produce the goal sentence.

Some basic logic identities for propositional calculus are:
∼ ∼ A ⇔ A (Double negative)
A ⇒ B ⇔ ∼ A ∨ B (⇔ elimination).
Proof: (A ⇒ B) ⇔ (∼ A ∨ B) F T F T F T F F T T T T T T T F F T F F F T T T T F T T

∼ (A ∧ B) ⇔ (∼ A ∨ ∼ B)
∼ (A ∨ B) ⇔ (∼ A ∧ ∼ B) (deMorgan's laws)
A ∨ (B ∧ C) ⇔ (A ∨ B) ∧ (A ∨ C)
A ∧ (B ∨ C) ⇔ (A ∧ B) ∨ (A ∧ C) (Distributive laws).

Normal Forms

A normal form is a canonical way to write a logical sentence. It turns out that any PC sentence can be written in either of the universal forms:

Conjunctive Normal Form (CNF): a conjunction of disjunctions of literals (proposition letters and their negations). Each disjunction of literals is a clause.
e.g. (A ∨ ∼ B) ∧ (B ∨ ∼ C ∨ ∼ D)

CNF is the needed representation for our two most important techniques for inference -- one for propositional logic (satisfiability solving) and one for both PL and FOL (resolution).

Disjunctive Normal Form (DNF): a disjunction of conjunctions of literals. Each conjunction of literals is a term.
Same e.g.
(A ∧ B) ∨ (A ∧ ∼ C) ∨ (A ∧ ∼ D) ∨
(∼ B ∧ ∼ C) ∨ (∼ B ∧ ∼ D)

Another normal form that does not allow every PC sentence to be represented but is practically important (e.g. Prolog, linear algorithms) is Horn Form: a conjunction of Horn Clauses (which have at most one positive literal): e.g.
(A ∨ ∼ B) ∧ (B ∨ ∼ C or ∼ D),
often written as a set of implications:
(B ⇒ A) and (C ∧ D) ⇒ B.
Which in turn can be interpreted top-down (to prove B, prove C and D) or bottom-up (if know C and D, can deduce B). The no-positive-literal form of a horn clause can be used in prolog: it seems to succeed or fail at consult- << prolog book, headless clauses and resolution proofs. resolution takes A->B and B->C to get A->C. or A->C and A to get C. How get null clause? headless clauses, like ->C to cancel C. >>

Horn clauses are closed under resolution, and inference can proceed through forward- or backward chaining in linear time.

More restricted than Horn clauses are Definite Clauses, which is a disjunction of literals of which exactly one is positive. In fact, these are the canonical Prolog rules. A Horn clause with no positive literals is not so useful in programming but is lurking in the idea of a proof by contradiction (which Prolog does behind the scenes: "at least one of these clauses must be false if this sentence is true"). Definite clauses look like "normal" prolog rules and can be interpreted as facts
(A, ∼ C) or implications
(A,B, C ⇒ D or in prolog
D :- A, B, C.

PC Inference Rules

Resolution Proofs

Example Resolution Proof

Control of Resolution Proofs

Teleport to Prop. Calc. Inference PPT Courtesy of Hwee Tou Ng (Nat. U. Singapore).