Hybrid and subexponential linear logics

Despeyroux, Joelle; Pimentel, Elaine Gouvea; Vega, Carlos Alberto Olarte

Hybrid and subexponential linear logics

Página do item simplificado Estatísticas

dc.contributor.author	Despeyroux, Joelle
dc.contributor.author	Pimentel, Elaine Gouvea
dc.contributor.author	Vega, Carlos Alberto Olarte
dc.date.accessioned	2020-07-30T18:10:25Z
dc.date.available	2020-07-30T18:10:25Z
dc.date.issued	2017
dc.description.resumo	HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In HyLL, truth judgments are labelled by worlds and hybrid connectives relate worlds with formulas. In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and an ordering on such labels defines the provability relation among resources in those locations. It is well known that SELL, as a logical framework, is strictly more expressive than LL. However, so far, it was not clear whether HyLL is more expressive than LL and/or SELL. In this paper, we show an encoding of the HyLL's logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also propose an encoding of HyLL into SELL (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. We conclude our expressiveness study by showing that previous attempts of encoding Computational Tree Logic (CTL) operators into HyLL cannot be extended to consider the whole set of temporal connectives. We show that a system of LL with fixed points is indeed needed to faithfully encode the behavior of such temporal operators	pt_BR
dc.identifier.citation	DESPEYROUX, Joëlle; OLARTE, Carlos; PIMENTEL, Elaine. Hybrid and Subexponential Linear Logics. Electronic Notes in Theoretical Computer Science, [S.L.], v. 332, p. 95-111, jun. 2017. Disponível em: https://www.sciencedirect.com/science/article/pii/S1571066117300178?via%3Dihub. Acesso em: 29 Jul. 2020. http://dx.doi.org/10.1016/j.entcs.2017.04.007.	pt_BR
dc.identifier.doi	10.1016/j.entcs.2017.04.007
dc.identifier.issn	1571-0661
dc.identifier.uri	https://repositorio.ufrn.br/jspui/handle/123456789/29756
dc.language	en	pt_BR
dc.publisher	Elsevier	pt_BR
dc.subject	Linear logic	pt_BR
dc.subject	Hybrid Linear Logic	pt_BR
dc.subject	Subexponentials	pt_BR
dc.subject	Logical frameworks	pt_BR
dc.subject	Temporal Logic	pt_BR
dc.title	Hybrid and subexponential linear logics	pt_BR
dc.type	article	pt_BR