Adams, A.A. (2000) A formalisation of weak normalisation (with respect to permutations) of sequent calculus proofs. LMS Journal of Computation and Mathematics, 3. pp. 1-26. ISSN 1461-1570Full text not available from this repository.
Dyckhoff and Pinto presents a weakly normalising system of reductions on derivations in the sequent calculus where the normal proofs 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. The formalisation has been kept as close as possible to the original presentation in order to evaluate the state of proof assistance for such methods, and to ensure similarity of methods not merely similarity of results. The formalisation is restricted to the implicational fragment of propositional intuitionistic logic.
|Subjects:||Mathematical and Computer Sciences > Others in Mathematical and Computing Sciences > Mathematical and Computing Sciences not elsewhere classified|
|Depositing User:||Dr Andrew Adams|
|Date Deposited:||23 Jul 2008 14:23|
|Last Modified:||23 Aug 2010 14:26|
Actions (login required)