Implementation and evaluation of contextual natural deduction for minimal logic

Bruno Woltzenlogel Paleo*

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Citation (Scopus)

    Abstract

    The contextual natural deduction calculus (NDc) extends the usual natural deduction calculus (ND) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. It has been shown that, asymptotically in the best case, NDc-proofs can be quadratically smaller than the smallest ND-proofs of the same theorems. In this paper we describe the first implementation of a theorem prover for minimal logic based on NDc. Furthermore, we empirically compare it to an equally simple ND theorem prover on thousands of randomly generated conjectures.

    Original languageEnglish
    Title of host publicationPerspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers
    EditorsManuel Mazzara, Andrei Voronkov
    PublisherSpringer Verlag
    Pages314-324
    Number of pages11
    ISBN (Print)9783319415789
    DOIs
    Publication statusPublished - 2016
    Event10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015 - Kazan and Innopolis, Russian Federation
    Duration: 24 Aug 201527 Aug 2015

    Publication series

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

    Conference

    Conference10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015
    Country/TerritoryRussian Federation
    CityKazan and Innopolis
    Period24/08/1527/08/15

    Fingerprint

    Dive into the research topics of 'Implementation and evaluation of contextual natural deduction for minimal logic'. Together they form a unique fingerprint.

    Cite this