Definition:Decision Procedure

Definition

Let $U$ be a set of propositional formulas.

A decision procedure for $U$ is an algorithm which, given a propositional formula $P$, always terminates, returning the answer:

• Yes if $P \in U$;
• No if $P \notin U$.

Refutation Procedure

A decision procedure can work like this.

From Tautology and Contradiction, if $P$ is true then $\neg P$ is false and vice versa.

Suppose we wish to decide if $P$ is valid.

We apply the decision procedure to $\neg P$.

If it reports that $\neg P$ is satisfiable, then $P$ is not valid (although it may be satisfiable).

If it reports that $\neg P$ is unsatisfiable, then $P$ is valid.

Such a decision procedure is called a refutation procedure.