Talk:Polarized linear logic
From LLWiki
(Difference between revisions)
(How to relate with the positive formula page) |
(About the presentation of LLP with a stoup) |
||
| Line 6: | Line 6: | ||
[[User:Olivier Laurent|Olivier Laurent]] 08:24, 5 October 2011 (UTC) |
[[User:Olivier Laurent|Olivier Laurent]] 08:24, 5 October 2011 (UTC) |
||
| + | |||
| + | == Stoup == |
||
| + | |||
| + | I am not sure I like the presentation with a stoup. I prefer to see the ''at most one formula'' property as a lemma consequence of the definition of the rules. |
||
| + | |||
| + | But maybe I am too much a fundamentalist in this topic ... |
||
| + | |||
| + | [[User:Olivier Laurent|Olivier Laurent]] 08:25, 5 October 2011 (UTC) |
||
Latest revision as of 09:25, 5 October 2011
[edit] Positive and negative formula
The notion of positive and negative formulas in polarized linear logic is a restriction of the more general one from linear logic. The relation might have to be clarified.
As mentioned in Talk:Positive_formula, we should also decide how to deal with the two dual notions.
Olivier Laurent 08:24, 5 October 2011 (UTC)
[edit] Stoup
I am not sure I like the presentation with a stoup. I prefer to see the at most one formula property as a lemma consequence of the definition of the rules.
But maybe I am too much a fundamentalist in this topic ...
Olivier Laurent 08:25, 5 October 2011 (UTC)
