The formal method of providing a proof in symbolic logic. It uses deductive inference. Each step in the proof will (a) introduce a premise or axiom; (b) provide a statement that is a natural consequence of previously established results using only legitimate rules of inference.

Such formal proofs are often long and tedious. Sophisticated programs known as theorem provers can be used to automate much of the process. See also mechanical verifier.