We present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SATsolver. Basically, it is obtained by adding a restart operation to the system intuit by Claessen and Ros´en, thus we call our implementation intuitR. We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform intuit and other state-of-the-art provers.

Efficient SAT-based Proof Search in Intuitionistic Propositional Logic / C. Fiorentini (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Automated Deduction – CADE 28 / [a cura di] A. Platzer, G. Sutcliffe. - Prima edizione. - [s.l] : Springer, 2021. - ISBN 9783030798758. - pp. 217-233 (( Intervento presentato al 28. convegno Conference on Automated Deduction tenutosi a Online nel 2021 [10.1007/978-3-030-79876-5_13].

Efficient SAT-based Proof Search in Intuitionistic Propositional Logic

C. Fiorentini
Primo
2021

Abstract

We present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SATsolver. Basically, it is obtained by adding a restart operation to the system intuit by Claessen and Ros´en, thus we call our implementation intuitR. We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform intuit and other state-of-the-art provers.
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
cade_2021_efficientSATbasedProofSearchIPL.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 577.44 kB
Formato Adobe PDF
577.44 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/855762
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact