We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based prover intuitR for IPL (Intuitionistic Propositional Logic). Given an intermediate logic L and a formula α, the procedure outputs either a Kripke countermodel for α or the instances of the characteristic axioms of L that must be added to IPL in order to prove α. The procedure exploits an incremental SAT-solver; during the computation, new clauses are learned and added to the solver.

SAT-Based Proof Search in Intermediate Propositional Logics / C. Fiorentini, M. Ferrari (LECTURE NOTES IN COMPUTER SCIENCE). - In: Automated Reasoning / [a cura di] J. Blanchette, L. Kovács , D. Pattinson. - [s.l] : Springer Cham, 2022. - ISBN 978-3-031-10768-9. - pp. 57-74 (( Intervento presentato al 11. convegno IJCAR tenutosi a Haifa nel 2022 [10.1007/978-3-031-10769-6_5].

SAT-Based Proof Search in Intermediate Propositional Logics

C. Fiorentini
Primo
;
M. Ferrari
Secondo
2022

Abstract

We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based prover intuitR for IPL (Intuitionistic Propositional Logic). Given an intermediate logic L and a formula α, the procedure outputs either a Kripke countermodel for α or the instances of the characteristic axioms of L that must be added to IPL in order to prove α. The procedure exploits an incremental SAT-solver; during the computation, new clauses are learned and added to the solver.
Settore MAT/01 - Logica Matematica
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
2022_IJCAR_SatBasedProofSearchIntermediateLogics.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 796.16 kB
Formato Adobe PDF
796.16 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: http://hdl.handle.net/2434/936783
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact