Symbolic reasoning

PL

PL : Propositional Logic

Atom :

• truth symbols : $\top$ True; $\bot$ False
• propositional varaibles

Literal : atom $\alpha$ and $\neg \alpha$

Formula (logical connective)

• not : $\neg$
• and : conjunction \and
• or : disjunction \or
• implies : implication $\Rightarrow$
• if and only if (iff): $\iff$

Syntax does not tell us the interpret of formula

Interpretation: mapping

$$I:\{P\to \text{true},Q\to \text{false}\}$$

Model:

• $I\models F$ : if $F$ evaluates to true under $I$

Satisfiability and Validity

$F$ is satisfiable iff there exists an interpretation $I$ such that $I\models F$

$F$ is valid iff all interpretations $I$, $I\models F$

Important relation:

$F$ is valid iff $\neg F$ is unsatisfiable

Truth Table

Satisfiability and Validity Checking : Method : Truth Tables

A proof method is sound if every formula that is proved true is valid

A proof method is complete if every valid formula has a proof

The truth table method for PL is sound and complete.

Decidability of PL

PL is decidable

There exists a method that can tell whether any formula in PL is valid (satisfiable)

The method is guarantee to halt within finite steps.

Not every logic is decidable.

Equivalence and Semantic Consequence

$F_1$ and $F_2$ is equivalent ($F_1\equiv F_2$) iff:

$$\{I\models F_1\}=\{I\models F_2\}$$

$F_1$ entails $F_2$ : $F_1\models F_2$ :

$$\{I\models F_1\}\subseteq \{I\models F_2\}$$

Translation to Formulas in Normal Forms

BNF : Backus Naor Form

NNF (Negation Normal Form) :

1. Eliminate Implication and bi-implication

F_1\to F_2\equiv \neg F_1\or F_2

F_1\leftrightarrow F_2=(F_1\to F_2)\and(F_2\to F_1)

2. Eliminate (double) negation

DNF (Disjunctive Normal Form) :

\Large{\or}_i\Large{\and}_j l_{i,j}

Final form is like : (\and\and)\or(\and \and)\or(\and)

CNF (Conjunctive Normal Form)

If clause has 1 literal is called unit clause

Tseitin Encoding :

Example :

(P_1\and P_2\cdots P_n)\or(Q_1\and Q_2\and\cdots Q_m)\equiv (P_1\or Q_1)\and(P_1\or Q_2)\and\cdots\and(P_n\or Q_m)

How many clauses in total do you have. $O(nm)$

But we can solve it to $O(3(n+m))$