FORMAL PROOF


FORMAL PROOF PRESENTATION


picto-b-130x130

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.

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

picto-9

Different interfaces have been developed to help with proof writing:

> Atelier B
> EMACSPRI (Obsolete)
> PROB
> RODIN PLATFORM PROVER