- English only

# Lab for Automated Reasoning and Analysis LARA

# Definition of Propositional Resolution

Recall:

**literal**is a propositional variable or its negation .**clause**is a disjunction of literals

## Clauses as Sets of Literals

The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas:

We therefore represent clauses as *sets of literals*. For example, we represent the clause as the set . We represent *false* as an empty clause and we do not represent *true*.

## Resolution Rule

Viewing clauses as sets, propositional resolution is the following rule:

Here are clauses and is a propositional variable.

Intuition: consider equivalent formulas

## Applying Resolution Rule to Check Satisfiability

Steps:

- If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability.
- Convert formula into polynomially large equisatisfiable formula in conjunctive normal form (see Normal Forms for Propositional Logic)
- Keep applying resolution rule until either
- empty clause is derived
- application of the resolution rule produces no new clauses

## Soundness of Resolution Rule

Suppose that and . If , then from we conclude and therefore . Similarly, if , then from we conclude and therefore .

Therefore, if and is the result of applying resolution rule to , then if and only if . Consequently, if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either.