Abstract | ||
---|---|---|
We study a fragment of Intuitionistic Linear Logic combined with non-normal modal operators. Focusing on the minimal modal logic, we provide a Gentzen-style sequent calculus as well as a semantics in terms of Kripke resource models. We show that the proof theory is sound and complete with respect to the class of minimal Kripke resource models. We also show that the sequent calculus allows cut elimination. We put the logical framework to use by instantiating it as a logic of agency. In particular, we apply it to reason about the resource-sensitive use of artefacts. |
Year | DOI | Venue |
---|---|---|
2014 | 10.3233/978-1-61499-419-0-723 | Frontiers in Artificial Intelligence and Applications |
Keywords | Field | DocType |
linear logic,agency | Intuitionistic logic,Mathematical optimization,Normal modal logic,Kripke semantics,Natural deduction,Computer science,Proof calculus,Multimodal logic,Algorithm,Theoretical computer science,Modal logic,Cut-elimination theorem | Conference |
Volume | ISSN | Citations |
263 | 0922-6389 | 5 |
PageRank | References | Authors |
0.50 | 19 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Daniele Porello | 1 | 90 | 23.55 |
Nicolas Troquard | 2 | 266 | 29.54 |