Rodin Handbook


3.4.1 Sequents

A sequent is a formal statement describing something we want to prove.

Sequents are of the following form

$H \vdash G$

where $H$ is the set of hypotheses (predicates) and $G$ is the goal that can be proved from the predicates.

The above statement can be read as follows: Under the hypotheses $H$, prove the goal $G$.