Machine checking proof theory: An application of logic to logic
Abstract
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.
Description
Citation
Collections
Source
The Proceedings of The 3rd Indian Conference on Logic and Its Applications (ICLA 2009)
Type
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31