Inference procedures for propositional logic

Our goal now is to decide whether $KB \models \alpha$ for some sentence $\alpha$.

Model checking

Reasoning with truth tables

Reasoning with truth tables is a form of semantic reasoning, in the sense that it directly exploits the definition of entailment: 𝛼 ⊨ 𝛽 holds when 𝛽 in every model that makes 𝛼 true.

In PL, a model is an assignment of truth values (1 or 0, true or false, 𝑇 or ⊥) to every propositional symbol that appears in 𝛼 or 𝛽 (or both)

Therefore, with 𝑛 symbols we have 2𝑛 different models, which correspond to the rows of the truth table

For every model (row), we compute the truth vales of 𝛼 and 𝛽 (by recursively computing the truth values of all the subsentences of 𝛼 and 𝛽) Then we have that 𝛼 ⊨ 𝛽 if, and only if, every model (row) that assigns 1 to 𝛼 also assigns 1 to 𝛽

Properties

This reasoning procedure is sound and complete. It always terminates, making reasoning in PL decidable.

However, it is inefficient when many propositional symbols are involved, because it has to compute a table of size 2𝑛×𝑀, where 𝑛 is the number of propositional symbols and 𝑀 is the number of subsentences the appear in the premises and the conclusion

Propositional satisfiability

Certain applications of PL require an agent to establish whether a set of sentences 𝛼 is or is not satisfiable

The problem of establishing the satisfiability of a set of propositional sentences is known as SAT Many interesting problems, including establishing propositional entailment, can be reduced to SAT

A (rather inefficient) solution of SAT is given by truth tables: 𝛼 is satisfiable if, and only if, it has truth value 1 in at least one row of its truth table

DPLL

Establish whether a set of sentences 𝛼 is or is not satisfiable

Preprocessing: convert every sentence in CNF (Conjunctive Normal Form)

Body of the procedure: from an empty assignment, incrementally try to build a model of 𝛼

• if a model is built, 𝛼 is satisfiable
• if the algorithm terminates without being able to build a model, 𝛼 is unsatisfiable

Conjunctive normal form (CNF)

CNF (Conjunctive Normal Form) represents a sentence as a conjunction of clauses, where a clause is a disjunction of literals and a literal is either a propositional symbol or the negation of a symbol.

Every sentence of propositional logic is logically equivalent to a conjunction of clauses.

• 𝐴 → 𝐵 ∨ 𝐶 becomes ¬𝐴 ∨ 𝐵 ∨ 𝐶
• 𝐶 → ¬𝐷 becomes ¬𝐶 ∨ ¬𝐷
• (𝐴 → 𝐵 ∨ 𝐶) ∧ (𝐶 → ¬𝐷) becomes ¬𝐴, 𝐵, 𝐶 , {¬𝐶, ¬𝐷}

Unit clause: clause with only one literal; e.g., ¬𝐶, 𝐶

The steps to convert to CNF are (Consider 𝐴 ↔ (𝐵 ∨ 𝐶)):

1. Eliminate ↔, replacing α ↔ 𝛽 with α → 𝛽 ∧ 𝛽 → α
   • (𝐴 → 𝐵 ∨ 𝐶 ) ∧ ( 𝐵 ∨ 𝐶 → 𝐴)
2. Eliminate →, replacing α → 𝛽 with ¬α ∨ 𝛽
   • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ (¬ 𝐵 ∨ 𝐶 ∨ 𝐴)
3. Move ¬ inwards using de Morgan's rules (¬ 𝛼 ∧ 𝛽 is equivalent to ¬α ∨ ¬𝛽 and ¬ 𝛼 ∨ 𝛽 is equivalent to ¬α ∧ ¬𝛽) and double-negation (¬¬𝛼 is equivalent to 𝛼)
   • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ ((¬𝐵 ∧ ¬𝐶) ∨ 𝐴)
4. Apply distributivity law (∧ over ∨) and flatten
   • (¬𝐴 ∨ 𝐵 ∨ 𝐶) ∧ (¬𝐵 ∨ 𝐴) ∧ (¬𝐶 ∨ 𝐴)

DPLL algorithm

Essentially a backtracking (depth-first) search over models with some extras:

• Early termination: stop when
  • all clauses are satisfied: (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) is satisfied by {𝐴 = 1}
  • any clause is falsified: (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) is falsified by {𝐴 = 0, 𝐵 = 0}
• Pure literals: if all occurrences of a symbol in yet-unsatisfied clauses have the same sign, then give the symbol that value
  • in (𝐴 ∨ 𝐵) ∧ (𝐴 ∨ ¬𝐶) ∧ (𝐶 ∨ ¬𝐵), 𝐴 is pure and positive, so set it to true
  • if there is a model, then there is a model also with {... , 𝐴 = 1, ... }
• Unit clauses: if a clause has a single literal, set the corresponding symbol to satisfy clause
  • in (𝐴 ∨ 𝐵) ∧ ¬𝐶, ¬𝐶 must be set to true {𝐶 = 0}

DPLL Example

Check if the set of sentences 𝛼 = {𝐴 → 𝐵 ∨ 𝐶, ¬𝐶, 𝐴 ∧ 𝐵 → 𝐷, 𝐶 → ¬𝐷} is satisfiable

Convert in CNF

• 𝐴 → 𝐵 ∨ 𝐶 becomes ¬𝐴 ∨ 𝐵 ∨ 𝐶
• ¬𝐶 becomes ¬𝐶
• 𝐴 ∧ 𝐵 → 𝐷 becomes ¬𝐴 ∨ ¬𝐵 ∨ 𝐷
• 𝐶 → ¬𝐷 becomes ¬𝐶 ∨ ¬𝐷

Assignments	Clauses	Rule
	¬A ∨ B ∨ C ¬C ¬A ∨ ¬B ∨ D ¬C ∨ ¬D	unit clause ¬C
¬C	¬A ∨ B T ¬A ∨ ¬B ∨ D T	pure literal ¬A
¬A	T T T T	early termination

Conclusion: the set of sentences 𝛼 = {𝐴 → 𝐵 ∨ 𝐶, ¬𝐶, 𝐴 ∧ 𝐵 → 𝐷, 𝐶 → ¬𝐷} is satisfiable (because it is satisfied by any complete assignment extending {¬𝐶 = 1, ¬𝐴 = 1})

Entailment via SAT

The problem of establishing propositional entailment can be reduced to a SAT problem, because 𝛼 ⊨ 𝛽 holds:

• if, and only if, every models that satisfies 𝛼 also satisfies 𝛽
• equivalently if, and only if, no model satisfies both 𝛼 and ¬𝛽
• equivalently if, and only if, 𝛼 ∧ ¬𝛽 is unsatisfiable

theorem-proving

Other than model checking entailment can be done by theorem proving—applying rules of inference directly to the sentences in our knowledge base to construct a proof of the desired sentence without consulting models. If the number of models is large but the length of the proof is short, then theorem proving can be more efficient than model checking.

1) Resolution

Resolution is similar to DPLL (when this is used to establish entailment): it starts from a CNF representation of the premises and the negation of the conclusion

Resolution applies (in all the possible ways) the resolution rule to the clauses (original ones and those derived by the previous applications of the resolution rule)

Suppose 𝐶1, 𝐶2 are clauses such that literal ℓ1 in 𝐶1 and literal ℓ2 in 𝐶2 are complementary (same propositional symbol with different sign), then clauses 𝐶1, 𝐶2 can be resolved into a new clause 𝐶 called resolvent C = (𝐶1 − {ℓ1}) ∪ (𝐶2 − {ℓ2})

Resolution properties

• Propositional resolution is an extremely powerful rule of inference for PL
• It works by refutation: to prove that KB ⊨ 𝛼 it proves that KB ∧ ¬𝛼 is unsatisfiable, namely it builds a refutation for KB ∧ ¬𝛼 by looking for the empty clause
• Using propositional resolution, it is possible to build a theorem prover that is sound and complete for PL
  • Resolution rule is sound
  • Theorem: resolvent 𝐶 is satisfiable if and only if clauses 𝐶1, 𝐶2 are simultaneously satisfiable
  • Since resolvent is smaller than parent clauses, resolution stops at some point
• Propositional resolution works on any set of sentences in clausal form (CNF)

2) Forward chaining

• Forward chaining considers definite clauses and applies Modus Ponens to generate new facts:
  • Modus Ponens: given 𝑋" ∧ 𝑋# ∧ ⋯ ∧ 𝑋$ → 𝑌 and 𝑋", 𝑋#, ..., 𝑋$, infer 𝑌
• Forward chaining keeps applying this rule, adding new facts, until nothing more can be added

Properties of forward chaining

Forward chaining is sound and complete for KBs composed of definite clauses

• Soundness: follows from soundness of Modus Ponens (easy to check)
• Completeness: the algorithm reaches a a fixed point from where no new atomic sentences can be derived

Forward chaining can only derive new positive literals (facts), it cannot derive new rules

3) Backward chaining

Backward chaining works like forward chaining, but backward:

• Start from the goal (query) 𝑞, which is a positive literal
• To prove 𝑞, check if 𝑞 is already in the KB, otherwise prove all the premises of a rule concluding 𝑞
• Avoid loops: check if new subgoal is already on the goal stack
• Avoid repeated work: check if new subgoal has already been proved true, or has already failed

Backward chaining is sound and complete for KBs composed of definite clauses