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:
Soundness: inference proves only true things.
Completeness: all true things can be proved.
More formally,
Soundness:
whenever
Completeness:
whenever
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
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.
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:
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 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.
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.
(∼ 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.
often written as a set of implications:
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
D :- A, B, C.
Teleport to Prop. Calc. Inference PPT Courtesy of Hwee Tou Ng (Nat. U. Singapore).