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

Camillo Fiorentini; Rajeev Goré; Stéphane Graham-Lengrand

doi:10.1007/978-3-030-29026-9_7

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 proceeding › Conference contribution › peer-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 language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings
Editors	Serenella Cerrito, Andrei Popescu
Publisher	Springer
Pages	111-129
Number of pages	19
ISBN (Print)	9783030290252
DOIs	https://doi.org/10.1007/978-3-030-29026-9_7
Publication status	Published - 2019
Event	28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 - London, United Kingdom Duration: 3 Sept 2019 → 5 Sept 2019

Publication series

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

Conference

Conference	28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019
Country/Territory	United Kingdom
City	London
Period	3/09/19 → 5/09/19

Access to Document

10.1007/978-3-030-29026-9_7

Cite this

Fiorentini, C., Goré, R., & Graham-Lengrand, S. (2019). A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. In S. Cerrito, & A. Popescu (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings (pp. 111-129). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11714 LNAI). Springer. https://doi.org/10.1007/978-3-030-29026-9_7

Fiorentini, Camillo ; Goré, Rajeev ; Graham-Lengrand, Stéphane. / A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings. editor / Serenella Cerrito ; Andrei Popescu. Springer, 2019. pp. 111-129 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{cbd10917ffe04ac1844645ae0a501bfe,

title = "A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic",

abstract = "Claessen and R{\'o}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.",

author = "Camillo Fiorentini and Rajeev Gor{\'e} and St{\'e}phane Graham-Lengrand",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 ; Conference date: 03-09-2019 Through 05-09-2019",

year = "2019",

doi = "10.1007/978-3-030-29026-9_7",

language = "English",

isbn = "9783030290252",

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

publisher = "Springer",

pages = "111--129",

editor = "Serenella Cerrito and Andrei Popescu",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings",

address = "Germany",

}

Fiorentini, C, Goré, R & Graham-Lengrand, S 2019, A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. in S Cerrito & A Popescu (eds), Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11714 LNAI, Springer, pp. 111-129, 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, London, United Kingdom, 3/09/19. https://doi.org/10.1007/978-3-030-29026-9_7

A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. / Fiorentini, Camillo; Goré, Rajeev; Graham-Lengrand, Stéphane.
Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings. ed. / Serenella Cerrito; Andrei Popescu. Springer, 2019. p. 111-129 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11714 LNAI).

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

TY - GEN

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

AU - Fiorentini, Camillo

AU - Goré, Rajeev

AU - Graham-Lengrand, Stéphane

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85077136724&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-29026-9_7

DO - 10.1007/978-3-030-29026-9_7

M3 - Conference contribution

SN - 9783030290252

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 111

EP - 129

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings

A2 - Cerrito, Serenella

A2 - Popescu, Andrei

PB - Springer

T2 - 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019

Y2 - 3 September 2019 through 5 September 2019

ER -

Fiorentini C, Goré R, Graham-Lengrand S. A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. In Cerrito S, Popescu A, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings. Springer. 2019. p. 111-129. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-29026-9_7

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this