Natural Deduction, Sharing By Presentation

Abstract

Part I of this thesis studies a fragment of natural deduction to which we have added the notion of sharing of subresults. This formalism is called 'deduction graphs'. We show some properties of cut-elimination on deduction graphs, like strong normalisation and confluence. We discuss connections with other formalisms, like Gentzen-Prawitz natural deduction, Fitch deduction, proof nets, lambda calculi and context calculi. Part II presents a case-study to the usability of computer formalised mathematics for education. The definitions and proofs of an interactive algebra course are replaced by their formal counterparts. Then, a complicated transformation process is used to make it human readable. The output is HTML and is accessible through the world wide web.