Rodin HandbookThis 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 
3.4.2 Proof RulesIn its pure mathematical form, a proof rule is a tool to perform a formal proof and is denoted by: where is a (possibly empty) list of sequents (the antecedents of the proof rule) and is a sequent (the consequent of the rule). We interpret the above proof rule as follows: The combination of the proofs of each sequent of prove the sequent .
3.4.2.1 Proof Rule Representation in RodinIn Rodin, the representation for proof rules is more structured not only to reduce the space required to store the rule but, more importantly, to support proof reuse. A proof rule in Rodin contains the following:
Each antecedent of the proof rule contains the following information:
With this representation, a proof rule in Rodin corresponding to a proof schema as follows: Where:
3.4.2.2 Applying Proof RulesGiven a proof rule of the form mentioned above, the following describes how to apply this rule to an input sequent. If the process is successful, a list of output sequences is produced.
