- English only

# Lab for Automated Reasoning and Analysis LARA

# Proof Theory for Propositional Logic

## Notion of a proof system

A set of proof rules, each of which specifies how to derive a formula from zero or more other formulas.

- Typical requirement: polynomial-time algorithm to check whether a rule application is valid according to the rule system

We write if we can derive formula in some proof system . We omit when it is clear.

Proof tree and proof sequences.

Proof complexity: given such that , the size of smallest proof of in .

## Soundness of a proof system

System is sound if for every formula ,

We can only prove true formulas.

## Completeness of a proof system

System is complete if for every formula ,

We can prove all valid formulas.

## Some Example Proof Systems

#### Case analysis proof system

A simple A sound and complete proof system.

**Rule 1:** Case analysis rule:

**Rule 2:** Evaluation rule: derive if has no variables and it evaluates to *true*.

We can also add simplification rules. Adding sound rules preserves soundness and completeness.

#### Gentzen proof system

Recall Gentzen's proof system from proofs and induction part of lecture02, ignoring rules for predicates and induction.