Now that we've seen how to express concepts as precise formulas; we would like to reason with them. By "reason", we mean some automated way of ascertaining or veriflying statements −−− some procedure that can be carried out on an unthinking computer that can only push around symbols. In particular, for propositional logic, we'll restrict our attention to some (closely related) problems:
- TAUTOLOGY: given a formula φ, is it a tautology?
- SATisfability: Give a formula φ, is it satisfable? (Is there some truth assignment to its variables, that makes it true?)
- EQUIV: Given two WFFs φ and ψ, are they equivalent? (Do they give the same result for all possible truth assignments to their variables?