Logic for Computer Scientists - Propositional Logic Basics

Formal Logic

Formal logic provides:

• A language to precisely express knowledge, requirements, facts
• A formal way to reason about consequences of given facts rigorously

Components:

• Syntax – how does a valid sentence look in the logic
• Semantics – what is the meaning of a sentence in the logic
• Proof System – a finite set of proof rules that derives (true) sentences using syntactic manipulations

Example: Traffic Light Logic

• Syntax:
  • 3 colours: green, red, yellow
• Semantics:
  • Red: stop, Yellow: if in the intersection leave immediately otherwise stop, Green: go
• Proof system:
  • if (in-the-intersection) then go!

The Prevalence of Logic in Software Engineering

• Hardware: The basics of how hardware works
• Programming Languages: The semantics of software (programming languages) is based on logic
• Algorithms: When developing algorithms and optimizations, many of them can be reduced to logic and solved effectively using automated decision procedures
• Requirements Engineering: In software engineering requirements and specification are sometimes defined using formal logic
• Software Verification: Testing and verification of software can be solved using logic-based decision procedures

Why study propositional logic?

Many computer programs can be formulated using propositional logic

• A program: a sequence of instructions
• An instruction: manipulates the memory
• At each moment the memory holds a state (8 bits ! 28 states)
• An instruction maps one state to another (memory manipulation)
• This manipulation can be demonstrated by a Boolean combinational circuit (hardware)
• We can encode a program that manipulates a memory with n bits as a propositional formula with n Boolean variables
• Your program can be implemented as a solver (SAT solver) that finds a solution for a given propositional formula

Studying propositional logic allows us to understand and use a SAT solver when necessary

• When is it necessary to use a SAT solver
• Using reduction to SAT (encoding) to solve an NP problem

Propositional Logic Basic

Propositional Logic Syntax

• An atomic formula has a form $A_i$, where $i=1,2,3$

• Formulas are defined inductively as follows:

  • All atomic formulas are formulas
  • For every formula $F, \neg F$ (called not $F$, negation of $F$ ) is a formula
  • For all formulas $F$ and $G, F \wedge G$ (called and) and $F \vee G$ (called or) are formulas

• Abbreviations

  • $A, B, C, \ldots = A_1, A_2,A_3,\ldots$
  • use $F_1 \rightarrow F_2$ instead of $\neg F_1 \vee F_2 \quad$ (implication)
  • use $F_1 \longleftrightarrow F_2$ instead of $\left(F_1 \rightarrow F_2\right) \wedge\left(F_2 \rightarrow F_1\right)$ (if and only if)
  • $\neg F$ is called negation of $F$. (not F)
  • $(F \wedge G)$ is the conjunction of $F$ and $G$. (AND)
  • $(F \vee G)$ is called disjunction of $F$ and $G$ (OR)

Any formula $F$ which occurs in another formula $G$ is called a subformula of $G$.

Propositional Logic Semantics

• Truth values: {0 (false), 1 (true)}
• $\mathbf{D}$ is any subset of the atomic formulas
• An assignment $\mathcal{A}$ is a function such that $\mathcal{A}( \mathbf{D}) = 0 \text{ or } 1$ (assigning true values).
  • e.g. $\mathcal{A}\left(A_i\right) = 1$
  • Note that $\mathcal{A}$ is different from $A$
• $\mathbf{E}$ ⊇ $\mathbf{D}$ set of formulas that can be built from $\mathbf{D}$
• An extended assignment $\mathcal{A}'$ such that $\mathcal{A}( \mathbf{E}) = 0 \text{ or } 1$ (assigning true values).
  • e.g. $\mathcal{A}'\left(A_i\right) = 1$
  • Note that $\mathcal{A}$ is different from $A$

For every atomic formula $A_i \in \mathbf{D}, \mathcal{A}^{\prime}\left(A_i\right)=\mathcal{A}\left(A_i\right)$.

$$\begin{aligned} & \mathcal{A}^{\prime}((F \wedge G))=\left\{\begin{array}{l} 1, \text { if } \mathcal{A}^{\prime}(F)=1 \text { and } \mathcal{A}^{\prime}(G)=1 \\ 0, \text { otherwise } \end{array}\right. \\ & \mathcal{A}^{\prime}((F \vee G))=\left\{\begin{array}{l} 1, \text { if } \mathcal{A}^{\prime}(F)=1 \text { or } \mathcal{A}^{\prime}(G)=1 \\ 0, \text { otherwise } \end{array}\right. \\ & \mathcal{A}^{\prime}(\neg F)=\left\{\begin{array}{l} 1, \text { if } \mathcal{A}^{\prime}(F)=0 \\ 0, \text { otherwise } \end{array}\right. \end{aligned}$$

Since $\mathcal{A}'$ is an extension of $\mathcal{A}$ ($\mathcal{A}$ and $\mathcal{A}'$ agree on $\mathbf{D}$), from now on, we drop the distinction between $\mathcal{A}$ and $\mathcal{A}'$ and just write $\mathcal{A}$ . (The reason for this temporary distinction was to be able to define $\mathcal{A}'$ formally.)

Truth Table

• A formula $\mathrm{F}$ with $n$ atomic sub-formulas has $2^n$ suitable assignments
• Build a truth table enumerating all assignments

Important Definitions

Let $F$ be a formula and let $\mathcal{A}$ be an assignment, i.e. a mapping from a subset of $\{A_1, A_2,...\}$ to {0,1}.

suitable

• An assignment $\mathcal{A}$ is suitable for a formula $F$ if $\mathcal{A}$ assigns a truth value to every atomic proposition of $F$

model

• If $\mathcal{A}$ is suitable for F, and if $\mathcal{A}(F) = 1$, then we write $\mathcal{A} \vDash F$. In this case we say F holds under the assignment $\mathcal{A}$, or $\mathcal{A}$ is model for F.
• Otherwise we write $\mathcal{A} \nvDash F$, and say: under the assignment $\mathcal{A}$, $F$ does not hold, or $\mathcal{A}$ is not a model for $F$.
• Therefore: An assignment $\mathcal{A}$ is a model for $F$, written $\mathcal{A} \vDash F$, if and only if
  • $\mathcal{A}$ is suitable for $F$
  • $\mathcal{A}(F)=1$, i.e., $F$ holds under $\mathcal{A}$

satisfiable

• A formula $F$ is satisfiable if and only if $F$ has a model, otherwise $F$ is unsatisfiable (or contradictory)

valid

• A formula $F$ is valid (or a tautology), written $\vDash F$, if and only if every suitable assignment for $\mathrm{F}$ is a model for $\mathrm{F}$
  • or if $\neg F$ is unsatisfiable.

Determining Satisfiability via a Truth Table

• F is satisfiable if and only if there is at least one entry with 1 in the truth table of F

Validity and Satisfiability

• Theorem: A formula F is valid if and only if ¬F is unsatifsiable

Equivalence

Formulas with different atomic propositions can be equivalent!

• all tautologies are equivalent to True
• all unsatisfiable formulas are equivalent to False
• but all satisfiable does not equivalent to True
  • two formulas can be true with different values on different rows of their truth tables

Semantic Equivalence

Substitution Theorem

Theorem:

1. Let F and G be equivalent formulas. Let H be a formula in which F occurs as a sub-formula.
2. Let H’ be a formula obtained from H by replacing every occurrence of F by G.
3. Then, H and H’ are equivalent.

Normal Forms

• A literal is either an atomic proposition $p$ or its negation $\neg p$
• A clause is a disjunction of literals
  • e.g., $p \vee \neg q \vee r$
• A formula is in Conjunctive Normal Form (CNF) if it is a conjunction of disjunctions of literals (i.e., a conjunction of clauses): $\bigwedge_{i=1}^n\left(\bigvee_{j=1}^{m_i} L_{i, j}\right.$ )
  • e.g., $(p \vee \neg q) \wedge(r \vee q)$

• A formula is in Disjunctive Normal Form (DNF) if it is a disjunction of conjunctions of literals: $\bigvee_{i=1}^n\left(\bigwedge_{j=1}^{m_i} L_{i, j}\right)$

Converting to Normal Forms

Theorem: For every formula F, there is an equivalent formula $F_1$ in CNF and $F_2$ in DNF

From Truth Tables to Normal Forms

• DNF: each entry in the truth table that is ‘1’ is a term in DNF, where the literals that are ‘0’ appear with negation, and themselves otherwise
• CNF (dual to DNF): each entry in the truth table that is ‘0’ is a term in CNF, where the literals that are ‘1’ appear with negation, and themselves otherwise

2-CNF Fragment

A formula F is in 2-CNF iff

• F is in CNF
• Every clause of F has at most 2 literals

Theorem: There is a polynomial algorithm for deciding whether a 2-CNF formula F is satisfiable

Not all formulas can be converted to 2-CNF

2-CNF is not NP-Complete

3-CNF Fragment

A formula F is in 3-CNF iff

• F is in CNF
• Every clause of F has at most 3 literals

Theorem: Deciding whether a 3-CNF formula F is satisfiable is at least as hard as deciding satisfiability of an arbitrary CNF formula G

Let G be an arbitrary CNF formula. Replace every clause of the form $\left(\mathscr{L}_0 \vee \ldots \vee \mathscr{L}_n\right)$ with 3-literal clauses

$$\left(\mathscr{L}_0 \vee b_0\right) \wedge\left(\neg b_0 \vee \mathscr{L}_1 \vee b_1\right) \wedge \ldots \wedge\left(\neg b_{n-1} \vee \mathscr{L}_n\right)$$

where $b_i$ are fresh atomic propositions not appearing in $\mathrm{F}$

3-CNF-SAT is NP-Complete

• Theorem: Determining the satisfiability of an arbitrary 3-CNF formula is an NP-complete problem.
• Application: If you can solve 3-CNF in polynomial time you can solve any NP problem in polynomial time!
• Encode a problem into a 3-CNF satisfiability problem
  • Use an automatic solver, so-called a SAT solver, to find a solution for your problem
  • No need to write an algorithm whatsoever, just call the SAT solver!
  • SAT solvers work for all forms of CNF!