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.
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic / C. Fiorentini, R. Goré, S. Graham-Lengrand (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Automated Reasoning with Analytic Tableaux and Related Methods / [a cura di] S. Cerrito, A. Popescu. - Prima edizione. - [s.l] : Springer, 2019 Aug. - ISBN 9783030290252. - pp. 111-129 (( Intervento presentato al 28. convegno TABLEAUX tenutosi a London nel 2019.
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic
C. Fiorentini;
2019
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
Fiorentini2019_Chapter_AProof-TheoreticPerspectiveOnS.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
968.16 kB
Formato
Adobe PDF
|
968.16 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
