Skip navigation
Skip navigation

Machine checking proof theory: An application of logic to logic

Gore, Rajeev

Description

Modern proof-assistants are now mature enough to formalise many aspects of mathematics. I outline some work we have done using the proof-assistant Isabelle to machine-check aspects of proof theory in general, and specifically the proof theory of provability logic GL.

CollectionsANU Research Publications
Date published: 2009
Type: Conference paper
URI: http://hdl.handle.net/1885/57625
Source: The Proceedings of The 3rd Indian Conference on Logic and Its Applications (ICLA 2009)
DOI: 10.1007/978-3-540-92701-3_2

Download

File Description SizeFormat Image
01_Gore_Machine_checking_proof_theory:_2009.pdf216.13 kBAdobe PDF    Request a copy
02_Gore_Machine_checking_proof_theory:_2009.pdf113.28 kBAdobe PDF    Request a copy
03_Gore_Machine_checking_proof_theory:_2009.pdf156.65 kBAdobe PDF    Request a copy
04_Gore_Machine_checking_proof_theory:_2009.pdf247.99 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator