Machine checking proof theory: An application of logic to logic
Date
2009
Authors
Gore, Rajeev
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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
Keywords
Keywords: Proof theories; Provability logic; Programming theory; Applications
Citation
Collections
Source
The Proceedings of The 3rd Indian Conference on Logic and Its Applications (ICLA 2009)
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31