FORMAL PROOF PRESENTATION
A formal proof activity is generally part of the formal validation activity, which consists in ensuring the validity of a theorem. Validation may be based on a number of techniques, the two main ones being formal proof and model checking.
Formal proof consists in demonstrating theorems with a proof assistant. Some of these tools allow for the automatic execution of portions (even the entirety) of a proof, but are most often used to validate proof established by the user so that a theorem is not proven in error.
A proof assistant is a tool with which a theorem description language and proof description language (which can be identical) are associated.
A certain number of proof assistants have been developed and are used within academia and industry. They can use a variety of techniques (see Formal Method on Wikipedia).
The particularity of B Method is that the lemmas that must be proven are produced by a tool (a proof obligation generator) in a language that corresponds to the first order logic associated with the set theory.
The proof tools used in the context of the method include:
> An inference rules database associated with a motor that includes heuristics
> A SAT-type prover