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