TY - GEN
T1 - Machine checking proof theory
T2 - 3rd Indian Conference on Logic and Its Applications, ICLA 2009
AU - Goré, Rajeev
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=59149096535&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-92701-3_2
DO - 10.1007/978-3-540-92701-3_2
M3 - Conference contribution
SN - 354092700X
SN - 9783540927006
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 23
EP - 35
BT - Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings
Y2 - 7 January 2009 through 11 January 2009
ER -