We present a proof search procedure for the minimal coreflection logic iCK4, an intuitionistic modal logic with the normality axiom and the coreflection principle. The procedure is based on a sequent calculus Gbu-iCK4 that ensures strong termination of backward proof search. Gbu-iCK4 is shown to be complete via a dual refutation calculus that enables the extraction of countermodels when the proof search fails. To support practical experimentation, we provide an implementation of the proof search and the countermodel extraction procedures.
Proof Search and Countermodel Construction for iCK4 / M. Ferrari, C. Fiorentini, P. Giardini (CEUR WORKSHOP PROCEEDINGS). - In: CILC 2025 : Italian Conference on Computational Logic 2025 / [a cura di] D. Guidotti, L. Pandolfo, L. Pulina. - Prima edizione. - [s.l] : CEUR Workshop Proceedings, 2025 Jul. - pp. 1-14 (( Intervento presentato al 40. convegno Italian Conference on Computational Logic tenutosi a Alghero nel 2025.
Proof Search and Countermodel Construction for iCK4
C. Fiorentini;
2025
Abstract
We present a proof search procedure for the minimal coreflection logic iCK4, an intuitionistic modal logic with the normality axiom and the coreflection principle. The procedure is based on a sequent calculus Gbu-iCK4 that ensures strong termination of backward proof search. Gbu-iCK4 is shown to be complete via a dual refutation calculus that enables the extraction of countermodels when the proof search fails. To support practical experimentation, we provide an implementation of the proof search and the countermodel extraction procedures.
| File | Dimensione | Formato | |
|---|---|---|---|
|
cilc2025.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Licenza:
Creative commons
Dimensione
1.33 MB
Formato
Adobe PDF
|
1.33 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
