University of Canterbury Home
    • Admin
    UC Research Repository
    UC Library
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    1. UC Home
    2. Library
    3. UC Research Repository
    4. College of Engineering
    5. Engineering: Theses and Dissertations
    6. View Item
    1. UC Home
    2.  > 
    3. Library
    4.  > 
    5. UC Research Repository
    6.  > 
    7. College of Engineering
    8.  > 
    9. Engineering: Theses and Dissertations
    10.  > 
    11. View Item

    Minimal logic and automated proof verification. (2019)

    Thumbnail
    View/Open
    Warren, Louis_PhD Thesis.pdf (455.0Kb)
    Type of Content
    Theses / Dissertations
    UC Permalink
    http://hdl.handle.net/10092/17558
    http://dx.doi.org/10.26021/2174
    Thesis Discipline
    Mathematics
    Degree Name
    Doctor of Philosophy
    Publisher
    University of Canterbury
    Language
    English
    Collections
    • Engineering: Theses and Dissertations [2462]
    Authors
    Warren, Louisshow all
    Abstract

    We implement natural deduction for first order minimal logic in Agda, and verify minimal logic proofs and natural deduction properties in the resulting proof system. We study the implications of adding the drinker paradox and other formula schemata to minimal logic. We show first that these principles are independent of the law of excluded middle and of each other, and second how these schemata relate to other well-known principles, such as Markov’s Principle of unbounded search, providing proofs and semantic models where appropriate. We show that Bishop’s constructive analysis can be adapted to minimal logic.

    Rights
    All Right Reserved
    https://canterbury.libguides.com/rights/theses
    Advanced Search

    Browse

    All of the RepositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThesis DisciplineThis CollectionBy Issue DateAuthorsTitlesSubjectsThesis Discipline

    Statistics

    View Usage Statistics
    • SUBMISSIONS
    • Research Outputs
    • UC Theses
    • CONTACTS
    • Send Feedback
    • +64 3 369 3853
    • ucresearchrepository@canterbury.ac.nz
    • ABOUT
    • UC Research Repository Guide
    • Copyright and Disclaimer
    • SUBMISSIONS
    • Research Outputs
    • UC Theses
    • CONTACTS
    • Send Feedback
    • +64 3 369 3853
    • ucresearchrepository@canterbury.ac.nz
    • ABOUT
    • UC Research Repository Guide
    • Copyright and Disclaimer