IV. Logic and proofs

2. Next, a step in a demonstration is defined by the concept of a "Sequent" having a set of named propositions (called "hypothesis") and list of propositions (to demonstrate) :

type Seq   = ((string*Prop) list) * (Prop list);;
let s1:Seq = ([],[p1]);;

A "proof" then consists in defining "deduction rules" that transform a sequent (:step in a demonstration) and succeed when the proposition to demonstrate is empty: sfinal=([...],[]).

2 - 12