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