%0 Book Section %1 gor'e_09_machine %A Gor'e, Rajeev %D 2009 %J Logic and Its Applications %K _to_download_springer 2009 %P 23--35 %R http://dx.doi.org/10.1007/978-3-540-92701-3_2 %T Machine Checking Proof Theory: An Application of Logic to Logic %U http://dx.doi.org/10.1007/978-3-540-92701-3_2 %X 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.

@incollection{gor'e_09_machine, 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.}, added-at = {2009-02-11T20:09:58.000+0100}, author = {Gor'{e}, Rajeev}, biburl = {https://www.bibsonomy.org/bibtex/2e46da6db9ce2aa3cb5509c348cf84da2/leonardo}, citeulike-article-id = {3914681}, doi = {http://dx.doi.org/10.1007/978-3-540-92701-3_2}, interhash = {f3bb5091469f97c56e837153727805f7}, intrahash = {e46da6db9ce2aa3cb5509c348cf84da2}, journal = {Logic and Its Applications}, keywords = {_to_download_springer 2009}, pages = {23--35}, posted-at = {2009-01-20 20:10:45}, priority = {2}, timestamp = {2009-02-11T20:09:58.000+0100}, title = {Machine Checking Proof Theory: An Application of Logic to Logic}, url = {http://dx.doi.org/10.1007/978-3-540-92701-3_2}, year = 2009 }