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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Goré, R. (2009). Machine checking proof theory: An application of logic to logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5378 LNAI, pp. 23–35). https://doi.org/10.1007/978-3-540-92701-3_2
Mendeley helps you to discover research relevant for your work.