Rule Based Reasoning

Entailment means that one thing follows from another:
KB ╞ α

Propositional Logic
--------------------

The proposition symbols P1, P2 etc are sentences
conjunction ^
disjunction V
implication (if-then) a -> b ≡ ~a V b // false iff a=T and b=F
biconditional a <-> b ≡ (a->b) ^ (b->a)

logically equivalent α ≡ ß iff α╞ β and β╞α

for:
1. (a ^ b) V (c V d)
2. (a V c V d) ^ (b V c V d)

We say we pick all the operand and operators after "a" except "^ b" since we are distributing over "^" in phrase "^ b" i.e. "a" operates on "V (c V d)" and "b" operates on the same phrase and the final operator is "^" which will go in the middle.

The same is true for the second example you mentioned...

1. (a ^ b) V (c ^ d) // Distribute over "^" in "a^b"
2. (a V (c ^ d)) ^ (b V (c ^ d)) // Expand
3. ((a V c)^(a V d)) ^ ((b V c)^(b V d)) // all operators outside parentheses are of type "^" so good to remove extra ones
4. (a V c) ^ (a V d) ^ (b V c) ^ (b V d)



A sentence is valid if it is true in all models (truth tables where α=True),

Validity is connected to inference via the Deduction Theorem:
KB ╞ α if and only if (KB ⇒ α) is valid

A sentence is satisfiable if it is true in some model

A sentence is unsatisfiable if it is true in no models

Satisfiability is connected to inference via the following:
KB ╞ α if and only if (KB ∧¬α) is unsatisfiable [] (empty clause)

Interpretation: any assignment of true and false to atoms

Rules of inference


Model checking
⌧truth table enumeration (always exponential in n)
⌧improved backtracking, e.g., Davis--Putnam-Logemann-Loveland (DPLL), Backtracking with constraint propagation, backjumping.
⌧heuristic search in model space (sound but incomplete)
e.g., min-conflicts-like hill-climbing algorithms

Resolution is sound

Resolution is NOT complete:
P and R entails P V R but you cannot infer P V R From (P and R) by resolution

Resolution is complete for refutation: adding (¬P) and (¬R) to (P and R) we can infer the empty clause. (proof by contradiction)

CNF = conjunctive normal form eg. (A V B) ^ C

( P ∧ ¬Q ) ∨ ( ¬R ∨ P ) ≡ ( P ∨ ¬ R ∨ P ) ∧ ( ¬ Q ∨ ¬R ∨ P ) ≡ ( P ∨ ¬R ), (¬Q ∨ ¬R ∨ P )

The set of support: those clauses coming from negation of the theorem or their decendents.

Horn clause: Eg C ^ (B -> A) ^ ( C ^ D -> B) NOT! (C V D -> B)

Forward chaining (data driven) - linear time
Idea: fire any rule whose premises are satisfied in the KB,
add its conclusion to the KB, until query is found

Backward chaining (goal driven) - linear time
Idea: work backwards from the query q:
to prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed


Efficient propositional inference:
- DPLL 1. early termination 2. purse symbol (same sign for everywhere, so either all nots or positives) 3. unit clause - clause with only a literal
- WalkSAT (incomplete), local search using randomness