Data di Pubblicazione:
2025
Citazione:
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.
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.
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.
Tipologia IRIS:
03 - Contributo in volume
Elenco autori:
M. Ferrari, C. Fiorentini, P. Giardini
Link alla scheda completa:
Link al Full Text:
Titolo del libro:
CILC 2025 : Italian Conference on Computational Logic 2025