# Questions tagged [linear-logic]

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

26 questions
Filter by
Sorted by
Tagged with
11 views

### What are the differences between a linear logic based planner and a first order logic based planner

Linear logic based planners and first order logic based planners must have different strengths and weaknesses. I would appreciate help in understanding what these strengths and weaknesses are and ...
41 views

### Distributive property of tensor ($\otimes$) over par (⅋) in linear logic

In the setting of linear logic, does $\otimes$ distribute over $⅋$? That is, is it possible to show that $$A \otimes (B ⅋ C) \stackrel?\equiv (A \otimes B) ⅋ (A \otimes C)$$ holds? If not, what ...
74 views

### Is $A \& B ⊸ A$ derivable?

Intuitively, the sentence $A \& B ⊸ A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any way to ...
104 views

### For every formula of linear logic, is there an equivalent formula in intuitionistic linear logic?

Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$...
122 views

### About the internal hom in a symmetric monoidal closed category

Let $\mathcal{C}$ be a symmetric monoidal closed category. My question is the following: Given three objects $X$, $Y$ and $Z$, and a morphism $f \colon Y \to Z$ in $\mathcal{C}$, does it ...
### How can we interpret that $A, B \vdash A, B$ is unprovable with resource interpretation in Linear Logic?
In Linear logic (LL), it is unprovable but when considering the resource interpretation it seems to me that from the resources $A, B$ we can produce the resources $A, B$. By $A, B \vdash A, B$ I mean ...