Simple tableaux for two expansions of Gödel modal logic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913212928098304 |
|---|---|
| author | Bilkova, Marta Ferguson, Thomas Kozhemiachenko, Daniil |
| author_facet | Bilkova, Marta Ferguson, Thomas Kozhemiachenko, Daniil |
| contents | This paper considers two logics. The first one, $\mathbf{K}\mathsf{G}_\mathsf{inv}$, is an expansion of the Gödel modal logic $\mathbf{K}\mathsf{G}$ with the involutive negation $\sim_\mathsf{i}$ defined as $v({\sim_\mathsf{i}}ϕ,w)=1-v(ϕ,w)$. The second one, $\mathbf{K}\mathsf{G}_\mathsf{bl}$, is the expansion of $\mathbf{K}\mathsf{G}_\mathsf{inv}$ with the bi-lattice connectives and modalities. We explore their semantical properties w.r.t. the standard semantics on $[0,1]$-valued Kripke frames and define a unified tableaux calculus that allows for the explicit countermodel construction. For this, we use an alternative semantics with the finite model property. Using the tableaux calculus, we construct a decision algorithm and show that satisfiability and validity in $\mathbf{K}\mathsf{G}_\mathsf{inv}$ and $\mathbf{K}\mathsf{G}_\mathsf{bl}$ are PSpace-complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_15395 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Simple tableaux for two expansions of Gödel modal logic Bilkova, Marta Ferguson, Thomas Kozhemiachenko, Daniil Logic This paper considers two logics. The first one, $\mathbf{K}\mathsf{G}_\mathsf{inv}$, is an expansion of the Gödel modal logic $\mathbf{K}\mathsf{G}$ with the involutive negation $\sim_\mathsf{i}$ defined as $v({\sim_\mathsf{i}}ϕ,w)=1-v(ϕ,w)$. The second one, $\mathbf{K}\mathsf{G}_\mathsf{bl}$, is the expansion of $\mathbf{K}\mathsf{G}_\mathsf{inv}$ with the bi-lattice connectives and modalities. We explore their semantical properties w.r.t. the standard semantics on $[0,1]$-valued Kripke frames and define a unified tableaux calculus that allows for the explicit countermodel construction. For this, we use an alternative semantics with the finite model property. Using the tableaux calculus, we construct a decision algorithm and show that satisfiability and validity in $\mathbf{K}\mathsf{G}_\mathsf{inv}$ and $\mathbf{K}\mathsf{G}_\mathsf{bl}$ are PSpace-complete. |
| title | Simple tableaux for two expansions of Gödel modal logic |
| topic | Logic |
| url | https://arxiv.org/abs/2401.15395 |