Definition:Decision Procedure
Definition
Let $S$ be a set of propositional formulas.
A decision procedure for $S$ is an algorithm which, given a propositional formula $\mathbf A$, always terminates, returning the answer:
- Yes if $\mathbf A \in S$;
- No if $\mathbf A \notin S$.
Decision Procedure for Satisfiability
Let $U$ be the set of satisfiable propositional formulas.
Then a decision procedure for $U$ is called a decision procedure for satisfiability.
Decision Procedure for Tautologies
Let $U$ be the set of propositional formulas that are tautologies.
Then a decision procedure for $U$ is called a decision procedure for tautologies.
Refutation Procedure
Given a decision procedure for satisfiability, one can craft a decision procedure for tautologies in the following way:
Suppose one wanted to decide if a propositional formula $\mathbf A$ is a tautology.
Then apply the given procedure to decide if its negation $\neg \mathbf A$ is satisfiable.
Now:
- If $\neg \mathbf A$ is not satisfiable, then by Tautology iff Negation is Unsatisfiable, $\mathbf A$ is a tautology.
- If $\neg \mathbf A$ is satisfiable, then by Satisfiable iff Negation is Falsifiable, $\mathbf A$ is falsifiable, so cannot be a tautology.
Hence we have crafted a decision procedure for tautologies.
Such a procedure is called a refutation procedure, because it proceeds by refuting, i.e. proving unsatisfiability of the negation of the formula at hand.
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.5.1$: Definition $2.40$