Proof Manager
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
Overview
Proof obligations are generated by the proof obligation generator and have the form of sequents.
Sequents are proved using Proof Rules.
The Proof Manager architecture is separated into two parts: extensible part and static part. The extensible part is responsible for generating individual proof rules. The static part is responsible for putting proof rules together to construct and manage proofs. We call components that generate valid proof rules Reasoners.
The basic reasoning capabilities of the Proof Manager can be extended by adding new reasoners. A reasoner may implement a decision procedure for automated proof, or a derived rule schema for interactive proof.
By applying the generated proof rules by different reasoner, the Proof Manager builds a (partial) proof for an proof obligation by constructing Proof Trees.
In order to encapsulate frequently used proof construction and manipulation steps, the Proof Manager provides the concept of Tactics. They provides high-level strategic proof manipulations. Adding new tactics is the second possibility for extending the Proof Manager.
Sequents
A sequent stands for something we want to prove.
Sequents are of the following form
where H is the set of hypotheses (predicates) and G is the goal (a predicate in the mathematical language).
The meaning of the above sequent is that: Under the hypotheses H, prove the goal G.
