Machine checking proof theory: An application of logic to logic

Rajeev Goré*

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-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 languageEnglish
    Title of host publicationLogic and Its Applications - Third Indian Conference, ICLA 2009, Proceedings
    Pages23-35
    Number of pages13
    DOIs
    Publication statusPublished - 2009
    Event3rd Indian Conference on Logic and Its Applications, ICLA 2009 - Chennai, India
    Duration: 7 Jan 200911 Jan 2009

    Publication series

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

    Conference

    Conference3rd Indian Conference on Logic and Its Applications, ICLA 2009
    Country/TerritoryIndia
    CityChennai
    Period7/01/0911/01/09

    Fingerprint

    Dive into the research topics of 'Machine checking proof theory: An application of logic to logic'. Together they form a unique fingerprint.

    Cite this