Machine checking proof theory: An application of logic to logic

Rajeev Goré

doi:10.1007/978-3-540-92701-3_2

Machine checking proof theory: An application of logic to logic

Rajeev Goré^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

2 Citations (Scopus)

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.

Original language	English
Title of host publication	Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings
Pages	23-35
Number of pages	13
DOIs	https://doi.org/10.1007/978-3-540-92701-3_2
Publication status	Published - 2009
Event	3rd Indian Conference on Logic and Its Applications, ICLA 2009 - Chennai, India Duration: 7 Jan 2009 → 11 Jan 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5378 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd Indian Conference on Logic and Its Applications, ICLA 2009
Country/Territory	India
City	Chennai
Period	7/01/09 → 11/01/09

Access to Document

10.1007/978-3-540-92701-3_2

Cite this

Goré, R. (2009). Machine checking proof theory: An application of logic to logic. In Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings (pp. 23-35). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5378 LNAI). https://doi.org/10.1007/978-3-540-92701-3_2

@inproceedings{8d59dd04a87b4b87a031c356e57f3ac1,

title = "Machine checking proof theory: An application of logic to logic",

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.",

author = "Rajeev Gor{\'e}",

year = "2009",

doi = "10.1007/978-3-540-92701-3\_2",

language = "English",

isbn = "354092700X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "23--35",

booktitle = "Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings",

note = "3rd Indian Conference on Logic and Its Applications, ICLA 2009 ; Conference date: 07-01-2009 Through 11-01-2009",

}

Goré, R 2009, Machine checking proof theory: An application of logic to logic. in Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5378 LNAI, pp. 23-35, 3rd Indian Conference on Logic and Its Applications, ICLA 2009, Chennai, India, 7/01/09. https://doi.org/10.1007/978-3-540-92701-3_2

Machine checking proof theory: An application of logic to logic. / Goré, Rajeev.
Logic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings. 2009. p. 23-35 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5378 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

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 - https://www.scopus.com/pages/publications/59149096535

U2 - 10.1007/978-3-540-92701-3_2

DO - 10.1007/978-3-540-92701-3_2

M3 - Conference Paper

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 -

Machine checking proof theory: An application of logic to logic

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this