Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/45218
Title: A uniform framework for substructural logics with modalities
Authors: Vega, Carlos Alberto Olarte
Lellmann, Björn
Pimentel, Elaine Gouvea
Keywords: Logical frameworks;Multimodalities;Linear nested sequents;Linear logic
Issue Date: 4-May-2017
Publisher: Easy Chair
Citation: VEGA, Carlos Alberto Olarte; LELLMANN, Björn; PIMENTEL, Elaine Gouvea. A uniform framework for substructural logics with modalities. In: INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING, 21., 2017. Anais [...] . S. L.: Epic Series In Computing, 2017. v. 46, p. 435-455. Disponível em: https://easychair.org/publications/paper/d5zT. Acesso em: 07 dez. 2021. DOI: https://doi.org/10.29007/93qg
Portuguese Abstract: It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, a ne, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring di erent axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for di erent logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems
Abstract: It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, a ne, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring di erent axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for di erent logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems
URI: https://repositorio.ufrn.br/handle/123456789/45218
ISSN: 2398-7340
Appears in Collections:CCET - DM - Trabalhos apresentados em eventos
ECT - Trabalhos apresentados em eventos

Files in This Item:
File Description SizeFormat 
UniformFrameworkSubstructural_VEGA_2016.pdf210.89 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.