Natural Deduction, Sharing By Presentation
In case you object to the disclosure of your thesis, you can contact email@example.com
[S.l.] : [S.n.]
Number of pages
VIII, 210 p.
Radboud University Nijmegen, 20 juni 2007
Promotor : Geuvers, J.H.
Display more detailsDisplay less details
Faculty of Science, Mathematics &Computing Science
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.
This item appears in the following Collection(s)
- Academic publications 
- Dissertations 
- Electronic publications 
- Faculty of Science 
- Open Access publications 
Upload full text
Use your RU credentials (u/z-number and password) to log in with SURFconext to upload a file for processing by the repository team.