Hybrid and subexponential linear logics

DOI10.1016/J.ENTCS.2017.04.007MaRDI QIDQ1744445zbMATH OpenOpenAlexDBLPWikidataFDO

Authors J. Despeyroux, Carlos Olarte, Elaine Pimentel

Publication date 23 April 2018

Full work available at URL https://arxiv.org/abs/1608.08779

zbMATH Keywords

linear logictemporal logicsubexponentialslogical frameworkshybrid linear logic

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

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.

Recommendations

• Hybrid linear logic, revisited
• On subexponentials, focusing and modalities in concurrent systems
• Specifying proof systems in linear logic with subexponentials
• Subexponential concurrent constraint programming
• Hybridizing a logical framework

Cites work

• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• A formal framework for specifying sequent calculus proof systems
• A general proof system for modalities in concurrent constraint programming
• A hybrid linear logic for constrained transition systems
• A linear logical framework
• A logical framework for systems biology
• A proof theoretic study of soft concurrent constraint programming
• A proof theoretic view of spatial and temporal dependencies in biochemical systems
• An adequate compositional encoding of bigraph structure in linear logic with subexponentials
• Classical and intuitionistic subexponential logics are equally expressive
• Foundations for reliable and flexible interactive multimedia scores
• Hybridizing a logical framework
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Specifying proof systems in linear logic with subexponentials
• Subexponential concurrent constraint programming
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(7)

• scientific article; zbMATH DE number 7649947 (Why is no real title available?)
• On subexponentials, focusing and modalities in concurrent systems
• Complexity and Succinctness Issues for Linear-Time Hybrid Logics
• Hybrid linear logic, revisited
• Mechanizing focused linear logic in Coq
• scientific article; zbMATH DE number 786488 (Why is no real title available?)
• A Survey of the Proof-Theoretic Foundations of Logic Programming

This page was built for publication: Hybrid and subexponential linear logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1744445)