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 PRESENTATION
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
Different interfaces have been developed to help with proof writing:
|Plug-in name||Version||Status||MCV||Release date|
|Atelier-B provers||2.3.0||Available||3.3.0||02 Dec 2020|