- English only

# Lab for Automated Reasoning and Analysis LARA

# Propositional Logic

Propositional logic is the core part of most logical formalisms (such as first-order and higher-order logic). It also describes well digital circuits that are the basis of most modern computing devices.

## Importance of Propositional Logic

- Many search problems can be encoded using propositional formulas
- Checking equivalence of logical combinatorial circuits in hardware directly reduces to SAT
- Can encode integer arithmetic with fixed bitwidth (e.g. operations on 16-bit integers)
- An important class of logics can be obtained by giving meaning to propositional variables

## Propositional Formulas

Propositional logic studies propositional formulas.

*Propositional formulas* are expressions built from

- constants
*true*and*false* - propositional variables, such as , , , , …
- logical operators () that combine propositional formulas into larger propositional formulas (we define their meaning below)

**Analogy with mathematical expressions:** Just like a mathematical expression such as specifies a binary function from values of and to the value , a propositional formula such as specifies a function from the values of and to the value .

## Definitions of Logical Operations (Logical Connectives)

We specify a binary logical operation by a truth table: for each combination of arguments we indicate the result of the operation. For binary operation, the rows indicate the first argument, the columns indicate the second argument.

#### Negation (logical 'not')

#### Conjunction (logical 'and')

#### Disjunction (logical 'or')

#### Implication ('if')

Check validity of these implications:

#### Logical Eqivalence ('if and only if')

## Evaluating Propositional Formulas

If we know values of variables in the formula, we can compute its value.

Let us evaluate formula

for all values of its parameters. Let us draw formula as a tree. We introduce a column for each tree node. We obtain the value of a tree node by looking at the value of its children and applying the truth table for the operation in the node. The root gives the truth value of the formula.

## Validity, Satisfiability of Logical Formulas

Formula is *valid* if it evaluates to *true* for *all* values of its variables (all columns for formula say *true*).

Formula is *satisfiable* if it evaluates to *true* for *some* values of its variables (*true* appears in at least one column).

Formula is *unsatisfiable* if it evaluates to *false* for *all* values of its variables (all columns for formula say *false*).

**Observations**

- is unsatisfiable if and only if is not satisfiable
- is valid if and only if is unsatisfiable

**SAT** problem: given a propositional formula , check whether is satisfiable.

**SAT** is a well-known NP-complete problem.

## Propositional Tautologies

Valid propositional formula is called *propositional tautology*, or *tautology* for short. Tautologies are basic principles of logical reasoning. They are true regardless of how complex the intended meaning of propositions is, as long as we are sure that each proposition evaluates to *true* or *false*.

Here is a small list of tautologies.

Suggest another tautology.

## More information

- Calculus of Computation Textbook, Chapter 1 (for now especially Sections 1.1, 1.2, 1.3)
- Gallier Logic Book, Sections 3.1, 3.2, 3.3