Publicação
On the Proof Theory of Modal Logics
| datacite.subject.fos | Ciências Naturais::Matemáticas | pt_PT |
| dc.contributor.advisor | Ferreira, Fernando | |
| dc.contributor.advisor | Girlando, Marianna | |
| dc.contributor.author | Costa, Maria Osório Oliveira | |
| dc.date.accessioned | 2024-07-22T15:44:09Z | |
| dc.date.available | 2024-07-22T15:44:09Z | |
| dc.date.issued | 2024 | |
| dc.date.submitted | 2024 | |
| dc.description | Tese de Mestrado, Matemática, 2024, Universidade de Lisboa, Faculdade de Ciências | pt_PT |
| dc.description.abstract | This thesis aims at presenting a proof-theoretical analysis of modal logics. Modal logics extend classical propositional logic by adding to the language operators ′□′ and ′♢ ′ , expressing necessity and possibility. In this work, we will be focusing on the modal logics in the S5-cube, built from the basic modal logic K by considering combinations of certain frame conditions such as reflexivity, symmetry and transitivity. We are interested in the study of sequent systems for this family of logics. The systems we present are based on Gentzen’s calculus G3cp, with two additional pairs of rules for the modal operators and where the language has been extended with labels. These labels annotate formulas denoting worlds in a Kripke-model where they are satisfied. Note that this idea is not limited to sequent calculi, in fact, it has been studied for other formal systems such as natural deduction [2, 3] and tableau [10]. Moreover, labels can represent, not only worlds in a model, but also truth values [28]. We discuss several results that have been obtained in the literature for this family of modal logics, such as admissibility of weakening, contraction, and most notably cut-admissibility, which ensures the subformula property. Furthermore, we investigate proof-search termination strategies, which allows us to obtain countermodels for non-derivable sequents, and prove, via proof-theoretical tools, decidability and the finite model property for the logics in the cube, in particular for K and S4 which we take as a case study. | pt_PT |
| dc.identifier.tid | 203683579 | |
| dc.identifier.uri | http://hdl.handle.net/10451/65400 | |
| dc.language.iso | eng | pt_PT |
| dc.relation | UIDP/04561/2020 | pt_PT |
| dc.subject | Teoria da demonstração | pt_PT |
| dc.subject | Lógica modal | pt_PT |
| dc.subject | Cálculo de sequentes | pt_PT |
| dc.subject | Dedução etiquetada | pt_PT |
| dc.subject | Decidibilidade | pt_PT |
| dc.subject | Teses de mestrado - 2024 | pt_PT |
| dc.title | On the Proof Theory of Modal Logics | pt_PT |
| dc.type | master thesis | |
| dspace.entity.type | Publication | |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | masterThesis | pt_PT |
| thesis.degree.name | Mestrado em Matemática | pt_PT |