A formalisation of weak normalisation (with respect to permutations) of sequent calculus proofs
A. A. Adams
Abstract: Dyckhoff and Pinto present a weakly normalising system
of reductions on derivations in the cut-free intuitionistic
sequent calculus, where the normal derivations
are characterised as the fixed points of the composition of the
Prawitz translations into natural deduction and back.
This paper presents a formalisation of the system, including a proof
of the weak normalisation property for the formalisation.
More details can be found in earlier work by the author.
The formalisation has been kept as close as possible to the original
presentation to allow an evaluation of the state of proof assistance for
such methods, and to ensure similarity of methods, and not merely similarity
of results.
The formalisation is restricted to the implicational
fragment of intuitionistic logic.
|
