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

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
Back to topicon-arrow-up-solid
 
APRU
IARU
 
edX
Group of Eight Member

Acknowledgement of Country

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.


Contact ANUCopyrightDisclaimerPrivacyFreedom of Information

+61 2 6125 5111 The Australian National University, Canberra

TEQSA Provider ID: PRV12002 (Australian University) CRICOS Provider Code: 00120C ABN: 52 234 063 906