English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logicalframeworks that have been extensively used for specifying systems that exhibitmodalities such as temporal or spatial ones. Both frameworks have linear logic(LL) as a common ground and they admit (cut-free) complete focused proofsystems. The difference between the two logics relies on the way modalities arehandled. In HyLL, truth judgments are labelled by worlds and hybrid connectivesrelate worlds with formulas. In SELL, the linear logic exponentials (!, ?) aredecorated with labels representing locations, and an ordering on such labelsdefines the provability relation among resources in those locations. It is wellknown 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 LLand/or SELL. In this paper, we show an encoding of the HyLL's logical rulesinto LL with the highest level of adequacy, hence showing that HyLL is asexpressive as LL. We also propose an encoding of HyLL into SELL $\doublecup$(SELL plus quantification over locations) that gives better insights about themeaning of worlds in HyLL. We conclude our expressiveness study by showing thatprevious attempts of encoding Computational Tree Logic (CTL) operators intoHyLL cannot be extended to consider the whole set of temporal connectives. Weshow that a system of LL with fixed points is indeed needed to faithfullyencode the behavior of such temporal operators.

Hybrid and Subexponential Linear Logics Technical Report