A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic

Camillo Fiorentini*, Rajeev Goré, Stéphane Graham-Lengrand

*Corresponding author for this work

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

    8 Citations (Scopus)

    Abstract

    Claessen and Rósen have recently presented an automated theorem prover, intuit, for intuitionistic propositional logic which utilises a SAT-solver. We present a sequent calculus perspective of the theory underpinning intuit by showing that it implements a generalisation of the implication-left rule from the sequent calculus LJT, also known as G4ip and popularised by Roy Dyckhoff.

    Original languageEnglish
    Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings
    EditorsSerenella Cerrito, Andrei Popescu
    PublisherSpringer
    Pages111-129
    Number of pages19
    ISBN (Print)9783030290252
    DOIs
    Publication statusPublished - 2019
    Event28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 - London, United Kingdom
    Duration: 3 Sept 20195 Sept 2019

    Publication series

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

    Conference

    Conference28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019
    Country/TerritoryUnited Kingdom
    CityLondon
    Period3/09/195/09/19

    Fingerprint

    Dive into the research topics of 'A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic'. Together they form a unique fingerprint.

    Cite this