| | |
| | |
Stat |
Members: 3667 Articles: 2'599'751 Articles rated: 2609
16 February 2025 |
|
| | | |
|
Article overview
| |
|
Hybrid and Subexponential Linear Logics Technical Report | Joëlle Despeyroux
; Carlos Olarte
; Elaine Pimentel
; | Date: |
2 Sep 2016 | Abstract: | 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 $doublecup$
(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. | Source: | arXiv, 1608.8779 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|