Formal Proof
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 Link).
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:
-
a
inference rules database associated with a motor that includes heuristics
-
a
SAT-type prover.
Different
interfaces have been developed to help with proof writing:
-
-
-
Click'n'Prove
-
Rodin platform prover (link)
