Propositional logic

Short summary of propositional logic

Propositional logic

a formal way for representing complex statements that can be true or false

complex=statements that can be expressed in terms of a number of facts that can be true or false

representing statements + reasoning about them

Boolean formulae in Java

int c;
if(a==0)
  c=0;
if(((b==0)&&(d!=0))||(a!=0))
  c=1;
System.out.println(c);

• simple conditions: a==0, b=0 and d==0
• negations: !
  a!=0 is the same as !(a==0)
• and (conjunction): &&
• or (disjunction): ||

Example of use of logic

Will this program compile?

int c;
if(a==0)
  c=0;
if(((b==0)&&(d!=0))||(a!=0))
  c=1;
System.out.println(c);

Example: initialization

int c;
if(a==0)
  c=0;
if(((b==0)&&(d!=0))||(a!=0))
  c=1;
System.out.println(c);

Compiler refuses to compile

Error: Variable c may not have been initialized

Meaning: c is only initialized within if conditional instructions; conditions might be false

May be false as far as the compiler knows!

Example: unsatisfiability of conditions

Compiler just assumes that every conditions could be false

In this case:

• if a is zero, c=0 is executed
• if a is not zero, c=1 is executed

No way to make both a==0 and (((b==0)&&(d!=0))||(a!=0)) false at the same time

Uses of logic

• check if a formula can be satisfied
• check if a formula is always true
• check if a formula entails another
• ...

Syntax

• variables, like x, y, z...
• connectives: ∧, ∨, ¬

Examples:

• (x ∨ ¬y) ∧ z
• (¬z ∧ ¬y) ∨ (¬x ∧ (z ∧ x))
• (z ∨ y ∨ ¬x) ∧ w ∧ (x ∨ ¬(¬y ∧ z))

Variables

Variables can be only true or false

Every elementary condition like a==0 is expressed by a variable, like x

No way to express what x means, just that it is a condition (something that can be true or false)

Semantics

Interpretation = evaluation of the variables

An interpretation I tells the value (true or false) of each variable

Example: I = {x=true, y=false, z=false}

Example: I' = {x=false, y=false, z=true}

Evaluation: I ⊨ F means that F is true when the variables have the values of I

If I ⊨ F, we say that I is a model of F

Reasoning

What can we do in propositional logic?

• checking whether a formula is true according to an interpretation
• checking whether a formula is satisfiable (=it is satisfied by at least an interpretation)
• checking whether a formula is valid (true for all interpretations)
• checking whether a formula implies another formula (F ⇒ G: every model of F is a model of G)

How about the example Java program?

int c;
if(a==0)
  c=0;
if(((b==0)&&(d!=0))||(a!=0))
  c=1;
System.out.println(c);

c is always initialized if (a==0)&&(((b==0)&&(d!=0))||(a!=0)) is always true

Propositional logic does not work with integers: express a==0, b==0 and d==0 by x, y and z, respectively

Is x ∧ ((y ∧ ¬z) ∨ ¬x) always true?

(yes)

not much useful in practice (just an example)

Other problems can be expressed in propositional logic:

• planning
• scheduling
• diagnosis

CNF form

Definition:

• A propositional CNF formula is a conjunction of clauses
• A clause is a disjunction of literals
• A literal is a variable or the negation of a variable

Example: (¬x ∨ y ∨ z) ∧ (x ∨ ¬z)

• ¬x, y, z, x, ¬z are literals
• ¬x ∨ y ∨ z is a clause, and so is x ∨ ¬z
• the whole formula is a conjunction of clauses

Set notation: omit ∧ by writing the set of clauses:

{¬x ∨ y ∨ z, x ∨ ¬z}

CNF: examples

• x (one clause, made of a single positive literal)
• x ∧ ¬y (two clauses, each made of a single literal, one positive and one literal)
• (¬z ∨ y ∨ w) ∧ (x ∨ y) ∧ (¬x ∨ z ∨ ¬w) (three clauses of three, two and three literals respectively)
• (x ∨ y ∨ z) ∧ ¬x ∧ y ∧ (w ∨ ¬y) (four clauses of three, one, one and two literals respectively)

CNF: conversion

Two methods:

• first converts every formula into an equivalent one that is in CNF (transformation may increase size exponentially)
• second converts every formula into an equisatisfiable one that is CNF with at most a polynomial increase of size
  (equisatisfiabile=one is satisfiable if and only if the other one is)

Equivalent conversion

works my "moving" connectives

if a connective is not in the right place:

¬

use De Morgan's laws:

1. ¬(A∧B)=¬A∨¬B
2. ¬(A∨B)=¬A∧¬B

∧ and ∨

use distributivity:

1. A∧(B∨C)=(A∧B)∨(A∧C)
2. A∨(B∧C)=(A∨B)∧(A∨C)

Equivalent conversion: example

policy:

• push in negation
• push in disjunctions (or, push out conjunctions)

Equivalent conversion: size

in the example, slight increase in formula size

in general: may be exponential

every distribution doubles (more or less) the size of the formula

result is exponential in the number of variables
(all possible disjunctions that contains either x₁ or x₂ and either x₃ or x₄ and…)

Equisatisfiable conversion

employs the connective ≡

A≡B = (A→B)∧(B→A)

can be expressed in terms of ∧, ∨ and ¬

conversion only needed for these two formulae

Equisatisfiable conversion: example

first push negation to literals (does not increase size)

as above (passages omitted)

for each subformula (apart literals), define a variable

resulting formula is obtained by:

1. conjoin the original formulae and these three
2. in all of them, replace each topmost subformula with its new variable

in this case, the result is the conjunction of:

• ¬x∨¬y∨x₁
• x₁ ≡ ¬z∧x₂
• x₂ ≡ ¬x∨x₃
• x₃ ≡ z∧y

Equisatisfiable conversion: size

result looks bigger (after converting ≡), but…

conversion increase size only linearly

no repeating doubling-size step, as in the first conversion

Equivalence?

second conversion does not preserve equivalence, but almost

• original formula does not contain x₁, x₂ and x₃
  every value for these variables would do
• the resulting formula contains x₃ ≡ z∧y
  values x₃=false, z=true and y=true falsifies it

apart from the new variables, models are the same