Rodin Handbook
This work is sponsored by the Deploy Project
This work is sponsored by the ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
Rodin User’s Handbook v.2.8 |  |
 |
 |
3.4.1 Sequents
A sequent is a formal statement describing something we want to prove.
Sequents are of the following form
where 
is the set of hypotheses (predicates) and 
is the goal that can be proved from the predicates.
The above statement can be read as follows: Under the hypotheses , prove the goal .
|
|
|
|
|
|