We introduce a natural deduction calculus for the G¨odelDummett Logic LC semantically characterized by linearly ordered Kripke models. Our calculus is inspired by an analogous calculus for Intuitionistic logic (IPL) internalizing mechanisms to reduce the proof-search space that has been used to define a goal-oriented proof-search procedure for IPL. In this paper we present the calculus for LC and we sketch its soundness and completeness.
A Natural Deduction Calculus for Godel-Dummett Logic Internalizing Proof-search Control Mechanisms / C. Fiorentini, M. Ferrari (CEUR WORKSHOP PROCEEDINGS). - In: CILC 2020 : Proceedings of CILC 2020 / [a cura di] F. Calimeri , S. Perri, E. Zumpano. - [s.l] : CEUR Workshop Proceedings, 2020. - pp. 91-104 (( Intervento presentato al 35. convegno Italian Conference on Computational Logic nel 2020.
A Natural Deduction Calculus for Godel-Dummett Logic Internalizing Proof-search Control Mechanisms
C. Fiorentini;M. Ferrari
2020
Abstract
We introduce a natural deduction calculus for the G¨odelDummett Logic LC semantically characterized by linearly ordered Kripke models. Our calculus is inspired by an analogous calculus for Intuitionistic logic (IPL) internalizing mechanisms to reduce the proof-search space that has been used to define a goal-oriented proof-search procedure for IPL. In this paper we present the calculus for LC and we sketch its soundness and completeness.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2020_CILC_NaturalDeductionGoedelLogic.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
574.31 kB
Formato
Adobe PDF
|
574.31 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
