<p>I know of work adding temporal modalities to linear logic to produce what has been called <em>temporal linear logic</em> (in contrast to LTL = linear-time temporal logic). This is quite interesting: a formula (without a modality) is interpreted as resources being available <em>now</em>. The next time modality $\bigcirc-$ is interpreted as resources being available in the next time step. The box modality $\Box-$ means that the resources can be consumed at any point in the future,
<em>determined by the holder of the resources</em>, whereas $\lozenge-$ means that the resources can be consumed at any point in time <em>determined by the system</em>. Notice the duality between the holder of the resource and the system.</p>

<ul>
<li><p>Banbara, M., Kang, K.-S., Hirai, T., Tamura, N.: <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.77.6666&amp;rep=rep1&amp;type=pdf" rel="nofollow">Logic programming in a fragment of intuitionistic temporal linear logic</a>. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 315–330. Springer, Heidelberg (2001)</p></li>
<li><p>Hirai, T.: <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.2107" rel="nofollow">Propositional temporal linear logic and its application to concurrent systems</a>. EICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Special Section on Concurrent Systems Technology) E83- A(11), 2219–2227 (2000)</p></li>
<li><p>Hirai, T.: <a href="http://kaminari.scitec.kobe-u.ac.jp/pub/hiraiPhD00.pdf" rel="nofollow">Temporal Linear Logic and Its Application</a>. PhD thesis, The Graduate School of Science and Technology, Kobe University, Japan (September 2000).</p></li>
<li><p>Kamide, N.: <a href="http://www.filozof.uni.lodz.pl/bulletin/pdf/v3634_08.pdf" rel="nofollow">Temporalizing Linear Logic</a> Bulletin of the Section of Logic Volume 36:3/4 (2007), pp. 173–182</p></li>
</ul>

<p>There are a few papers adding all sorts of modalities to linear and affine logic:</p>

<ul>
<li><p>Kamide, N.: <a href="http://portal.acm.org/citation.cfm?id=1143365" rel="nofollow">Linear and affine logics with temporal, spatial and epistemic logics</a>. Theoretical Computer Science 252, 165–207 (2006).</p></li>
<li><p>Kamide, N: <a href="http://logcom.oxfordjournals.org/content/14/5/625.full.pdf" rel="nofollow">Combining Soft Linear Logic and Spatio-Temporal Operators</a>. J Logic Computation (2004) 14 (5): 625-650.</p></li>
</ul>

<p>The work on temporal linear logic has been applied in agent-oriented programming and coordination, making essential use of the interpretation of the modalities described above:</p>

<ul>
<li><p>Kungas, P.: <a href="http://www.springerlink.com/index/r87l9g0mw7mvknr6.pdf" rel="nofollow">Temporal linear logic for symbolic agent negotiation</a>. In: Zhang, C., W. Guesgen, H., Yeap, W.-K. (eds.) PRICAI 2004. LNCS, vol. 3157, pp. 23–32. Springer, Heidelberg (2004)</p></li>
<li><p>Pham, D.Q., Harland, J., Winikoff, M.: <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.9407&amp;rep=rep1&amp;type=pdf" rel="nofollow">Modelling agent’s choices in temporal linear logic</a>. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2007. LNCS, vol. 4897, pp. 140–157. Springer, Heidelberg (2008)</p></li>
<li><p>Clarke, D. <a href="https://lirias.kuleuven.be/handle/123456789/217971" rel="nofollow">Coordination: Reo, Nets and Logic</a>. 
FMCO proceedings, LNCS, vol.  5382. (2008)</p></li>
</ul>

CC BY-SA 3.0
2011-04-05T13:56:57.953Z
2011-04-18T16:16:28.813Z
2011-04-18T16:16:28.813Z
Dave Clarke
<p>The !A modality of linear logic is a box operator satisfying the S4 axioms. </p>

<p>It's well-known that the uniqueness of !A is not derivable -- that is, if you have a red bang and a blue bang, both of which separately satisfy the rules for bang, you can't prove that they are equivalent. I don't recall offhand where this result can be found, but it's probably in Girard's 1987 paper on linear logic.</p>

<p>EDIT: I asked Jason Reed, whose thesis was about encodings of linear logic into hybrid logic, and he pointed me at the following paper by Chaudhuri and Despeyroux, <a href="http://www.lix.polytechnique.fr/~kaustuv/papers/tr09stores.pdf">"A Logic for Constrained Process Calculi with Applications to Molecular Biology"</a>. They extend intuitionistic linear logic with hybrid annotations intended to mirror temporal logic, and they did a very clean job of it -- they prove not just have cut-elimination, but also focalization. So it looks like it should be straightforward to simplify their calculus to get modal K a la Simpson. </p>

CC BY-SA 2.5
2011-04-01T10:44:04.707Z
I'm looking for something weaker, that corresponds to K rather than S4.
Rob
CC BY-SA 3.0
2011-04-14T06:38:58.080Z
@Rob: some weaker modalities for linear logic are studied in light linear logic.  I've seen a paper outlining the relationship between three LLLs and standard Kripkean modal logics, but I forget which and whether K was among them.
Charles Stewart
CC BY-SA 3.0
2011-05-04T08:48:49.620Z
@Charles: do you have the reference for that paper?
Rob
CC BY-SA 3.0
2011-05-04T10:29:06.980Z
@Rob: No, I'm afraid.  It occurs to me that it might have been a workshop paper that wasn't written up.  There's a paper by Danos & Joinet (2001) that lists some weak linear logics, [Linear Logic & Elementary Time](http://www.pps.jussieu.fr/~danos/pdf/ell.pdf), and you might figure out the axiomatics from that: it should follow by looking to see which are the theorems of the form Lp -> Rp, where L&R any any string of modal operators, and see which similar theorems of regular modal logic they match.
Charles Stewart
CC BY-SA 3.0
2011-05-06T18:13:56.190Z
@Charles - thanks! I will take a look at it.
Rob
CC BY-SA 2.5
2011-04-01T10:32:25.317Z
2011-04-05T13:37:10.697Z
2011-04-05T13:37:10.697Z
Neel Krishnaswami
<p>These kind of logics are considered in linguistics: you can have a look at Michael Moortgat's article, <a href="http://www.let.uu.nl/~Michael.Moortgat/personal/Courses/CG08/Docs/lola-ch2.pdf">Categorial Type Logic</a>.</p>

CC BY-SA 2.5
2011-04-01T10:30:42.777Z
2011-04-01T10:30:42.777Z
Noam Zeilberger
<p>I've been skimming Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", <em>Journal of Logic, Language and Information 11 (4)</em>, 2002, which isn't quite what I wanted, but the references cite Marcello D'Agostino and Dov M. Gabbay and Alessandra Russo, "Grafting Modalities onto substructural implication systems", <em>Studia Logica 59</em>, 1996, which seems to be what I am looking for. It is on CiteSeer <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719</a></p>

CC BY-SA 2.5
2011-04-01T10:43:07.950Z
2011-04-01T10:43:07.950Z
Rob
<p>Currently, the most systematic proof theory that allows many modal logics to be layered upon many substructural logics is Belnap's display logic, which has received a decent treatment at the hands of <a href="http://wwwhomes.uni-bielefeld.de/mkracht/html/veroeff-math-en.html" rel="nofollow">Marcus Kracht</a> &mdash;see in particular his <em>Power and Weakness of the Modal Display Logic</em>, 1996&mdash; and Heinrich Wansing, <a href="http://books.google.de/books?id=zSOvc06waIEC&amp;printsec=frontcover&amp;dq=display+logic+modal+logic+wansing&amp;source=bl&amp;ots=ewcX3mipur&amp;sig=-wPL8U4kfH3mH2vTshl7e8bRKUE&amp;hl=en&amp;ei=CJimTeu5GJCMswaW_JTlAQ&amp;sa=X&amp;oi=book_result&amp;ct=result&amp;resnum=1&amp;ved=0CBMQ6AEwAA" rel="nofollow"><em>Displaying Modal Logic</em></a>, 1998.</p>

<p>Display logic has problems handling noncommutative logic, which was one of the motivations behind a couple of MSc theses I supervised some years back, to apply some ideas about representing modalities in the Calculus of Structures, which is very powerful for representing substructural logics, but ran into problems because of the unusual way cut-elimination is proven in that setting.  Robert Hein's work on generating rules for modal logics from families of axioms, summarised in <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.3730" rel="nofollow">Purity through Unravelling</a>, 2005, covers most of the usual logics (the most important axioms not covered are B, CR, and L), and there is fairly strong circumstantial evidence to believe the cut-elimination conjecture.  None of this work actually treats substructural logic, but if a stronger kind of cut-elimination theorem were proven for these modalities, the so-called splitting lemma, this would make the logic very modular and cut-elimination should follow easily for all ways of gluing together the logics.</p>

<p>Substructural logic doesn't really have a uniform notion of semantics, but for modal substructural logic we do have a kind of recipe for turning semantics of the base logic into semantics of matching modal logics, by extending a trace-like semantics with a notion of frame or an algebraic/categorical semantics with a notion of operator.  Kracht and Wansing do some work in both of these directions.</p>

CC BY-SA 3.0
2011-04-14T07:41:29.073Z
2015-08-28T14:18:15.447Z
2015-08-28T14:18:15.447Z
Charles Stewart
<p>I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. substructural K (something like MALL with box operator, necessitation and K rules).</p>

<reference-request><lo.logic><proof-theory>
Looking for papers and articles on modal substructural logics
Rob
# Looking for papers and articles on modal substructural logics

(Asked by: username_0 on 2011-04-01)

I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. substructural K (something like MALL with box operator, necessitation and K rules).

**Tags:** reference-request, lo.logic, proof-theory


---

## 5 answers

### Answer by username_1 on 2011-04-05. Score: 13

I know of work adding temporal modalities to linear logic to produce what has been called *temporal linear logic* (in contrast to LTL = linear-time temporal logic). This is quite interesting: a formula (without a modality) is interpreted as resources being available *now*. The next time modality $\bigcirc-$ is interpreted as resources being available in the next time step. The box modality $\Box-$ means that the resources can be consumed at any point in the future,
*determined by the holder of the resources*, whereas $\lozenge-$ means that the resources can be consumed at any point in time *determined by the system*. Notice the duality between the holder of the resource and the system.

* Banbara, M., Kang, K.-S., Hirai, T., Tamura, N.: [Logic programming in a fragment of intuitionistic temporal linear logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.77.6666&rep=rep1&type=pdf). In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 315–330. Springer, Heidelberg (2001)
* Hirai, T.: [Propositional temporal linear logic and its application to concurrent systems](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.2107). EICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Special Section on Concurrent Systems Technology) E83- A(11), 2219–2227 (2000)
* Hirai, T.: [Temporal Linear Logic and Its Application](http://kaminari.scitec.kobe-u.ac.jp/pub/hiraiPhD00.pdf). PhD thesis, The Graduate School of Science and Technology, Kobe University, Japan (September 2000).
* Kamide, N.: [Temporalizing Linear Logic](http://www.filozof.uni.lodz.pl/bulletin/pdf/v3634_08.pdf) Bulletin of the Section of Logic Volume 36:3/4 (2007), pp. 173–182

There are a few papers adding all sorts of modalities to linear and affine logic:

* Kamide, N.: [Linear and affine logics with temporal, spatial and epistemic logics](http://portal.acm.org/citation.cfm?id=1143365). Theoretical Computer Science 252, 165–207 (2006).
* Kamide, N: [Combining Soft Linear Logic and Spatio-Temporal Operators](http://logcom.oxfordjournals.org/content/14/5/625.full.pdf). J Logic Computation (2004) 14 (5): 625-650.

The work on temporal linear logic has been applied in agent-oriented programming and coordination, making essential use of the interpretation of the modalities described above:

* Kungas, P.: [Temporal linear logic for symbolic agent negotiation](http://www.springerlink.com/index/r87l9g0mw7mvknr6.pdf). In: Zhang, C., W. Guesgen, H., Yeap, W.-K. (eds.) PRICAI 2004. LNCS, vol. 3157, pp. 23–32. Springer, Heidelberg (2004)
* Pham, D.Q., Harland, J., Winikoff, M.: [Modelling agent’s choices in temporal linear logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.9407&rep=rep1&type=pdf). In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2007. LNCS, vol. 4897, pp. 140–157. Springer, Heidelberg (2008)
* Clarke, D. [Coordination: Reo, Nets and Logic](https://lirias.kuleuven.be/handle/123456789/217971).
  FMCO proceedings, LNCS, vol. 5382. (2008)


---

### Answer by username_2 on 2011-04-01. Score: 8

The !A modality of linear logic is a box operator satisfying the S4 axioms.

It's well-known that the uniqueness of !A is not derivable -- that is, if you have a red bang and a blue bang, both of which separately satisfy the rules for bang, you can't prove that they are equivalent. I don't recall offhand where this result can be found, but it's probably in Girard's 1987 paper on linear logic.

EDIT: I asked Jason Reed, whose thesis was about encodings of linear logic into hybrid logic, and he pointed me at the following paper by Chaudhuri and Despeyroux, ["A Logic for Constrained Process Calculi with Applications to Molecular Biology"](http://www.lix.polytechnique.fr/~kaustuv/papers/tr09stores.pdf). They extend intuitionistic linear logic with hybrid annotations intended to mirror temporal logic, and they did a very clean job of it -- they prove not just have cut-elimination, but also focalization. So it looks like it should be straightforward to simplify their calculus to get modal K a la Simpson.

> **Comments:**
> **username_0**: I'm looking for something weaker, that corresponds to K rather than S4.  
> **username_3**: @username_0: some weaker modalities for linear logic are studied in light linear logic.  I've seen a paper outlining the relationship between three LLLs and standard Kripkean modal logics, but I forget which and whether K was among them.  
> **username_0**: @Charles: do you have the reference for that paper?  
> **username_3**: @username_0: No, I'm afraid.  It occurs to me that it might have been a workshop paper that wasn't written up.  There's a paper by Danos & Joinet (2001) that lists some weak linear logics, [Linear Logic & Elementary Time](http://www.pps.jussieu.fr/~danos/pdf/ell.pdf), and you might figure out the axiomatics from that: it should follow by looking to see which are the theorems of the form Lp -> Rp, where L&R any any string of modal operators, and see which similar theorems of regular modal logic they match.  
> **username_0**: @Charles - thanks! I will take a look at it.  

---

### Answer by username_4 on 2011-04-01. Score: 8

These kind of logics are considered in linguistics: you can have a look at Michael Moortgat's article, [Categorial Type Logic](http://www.let.uu.nl/~Michael.Moortgat/personal/Courses/CG08/Docs/lola-ch2.pdf).


---

### Answer by username_3 on 2011-04-14. Score: 7

Currently, the most systematic proof theory that allows many modal logics to be layered upon many substructural logics is Belnap's display logic, which has received a decent treatment at the hands of [Marcus Kracht](http://wwwhomes.uni-bielefeld.de/mkracht/html/veroeff-math-en.html) —see in particular his *Power and Weakness of the Modal Display Logic*, 1996— and Heinrich Wansing, [*Displaying Modal Logic*](http://books.google.de/books?id=zSOvc06waIEC&printsec=frontcover&dq=display+logic+modal+logic+wansing&source=bl&ots=ewcX3mipur&sig=-wPL8U4kfH3mH2vTshl7e8bRKUE&hl=en&ei=CJimTeu5GJCMswaW_JTlAQ&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBMQ6AEwAA), 1998.

Display logic has problems handling noncommutative logic, which was one of the motivations behind a couple of MSc theses I supervised some years back, to apply some ideas about representing modalities in the Calculus of Structures, which is very powerful for representing substructural logics, but ran into problems because of the unusual way cut-elimination is proven in that setting. username_0ert Hein's work on generating rules for modal logics from families of axioms, summarised in [Purity through Unravelling](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.3730), 2005, covers most of the usual logics (the most important axioms not covered are B, CR, and L), and there is fairly strong circumstantial evidence to believe the cut-elimination conjecture. None of this work actually treats substructural logic, but if a stronger kind of cut-elimination theorem were proven for these modalities, the so-called splitting lemma, this would make the logic very modular and cut-elimination should follow easily for all ways of gluing together the logics.

Substructural logic doesn't really have a uniform notion of semantics, but for modal substructural logic we do have a kind of recipe for turning semantics of the base logic into semantics of matching modal logics, by extending a trace-like semantics with a notion of frame or an algebraic/categorical semantics with a notion of operator. Kracht and Wansing do some work in both of these directions.


---

### Answer by username_0 on 2011-04-01. Score: 6

I've been skimming Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", *Journal of Logic, Language and Information 11 (4)*, 2002, which isn't quite what I wanted, but the references cite Marcello D'Agostino and Dov M. Gabbay and Alessandra Russo, "Grafting Modalities onto substructural implication systems", *Studia Logica 59*, 1996, which seems to be what I am looking for. It is on CiteSeer <http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719>


---

