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. FiorentiniPrimo
;M. FerrariSecondo
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.
| 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
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
