Machine checking proof theory: An application of logic to logic
-
Altmetric Citations
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.
Collections | ANU 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 | Size | Format | Image |
---|---|---|---|---|
01_Gore_Machine_checking_proof_theory:_2009.pdf | 216.13 kB | Adobe PDF | Request a copy | |
02_Gore_Machine_checking_proof_theory:_2009.pdf | 113.28 kB | Adobe PDF | Request a copy | |
03_Gore_Machine_checking_proof_theory:_2009.pdf | 156.65 kB | Adobe PDF | Request a copy | |
04_Gore_Machine_checking_proof_theory:_2009.pdf | 247.99 kB | Adobe 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