Three types of computer programs have been devised in order to make the generation of formal proofs easier. The simplest are proof checkers, which verify proofs step by step. The most ambitious are proof generators, which take an unproven proposition, and attempt to output a proof that the proposition is true, or a proof that it is false. Perhaps the most useful are proof assistants, interactive programs that help the user to develop proofs.
|
|
|