Definition:Decision Procedure/Refutation Procedure
Jump to navigation Jump to search
- 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.