Non-normal modalities in variants of linear logic. (English) Zbl 1398.03208
Summary: This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the logical framework to use by instantiating it as logics of agency. In particular, we propose a logic to reason about the resource-sensitive use of artefacts and illustrate it with a variety of examples.
MSC:
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
| 03B45 | Modal logic (including the logic of norms) |
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03F05 | Cut-elimination and normal-form theorems |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Abrusci, V. M., & Ruet, P. (1999). Non-commutative logic I: The multiplicative fragment. Annals of Pure and Applied Logic,101, 29-64. · Zbl 0962.03054 |
| [2] | Arló-Costa, H. L., & Pacuit, E. (2006). First-order classical modal logic. Studia Logica,84, 171-210. · Zbl 1122.03011 |
| [3] | Avron, A. (1988). The semantics and proof theory of linear logic. Theoretical Computer Science,57, 161-184. · Zbl 0652.03018 |
| [4] | Béchet, D., de Groote, P., & Retoré, C. (1997). A complete axiomatisation for the in-clusion of series-parallel partial orders. In H., Comon (Ed.), Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, proceedings. (pp. 230-240). Berlin Heidelberg: Springer. · Zbl 1379.06001 |
| [5] | Belnap, N., Perloff, M., & Xu, M. (2001). Facing the future: Agents and choices in our indeterminist world. Oxford: Oxford University Press. |
| [6] | Benton, N., Bierman, G., De Paiva, V., & Hyland, M. (1993). A term calculus for intuitionistic linear logic. In M. Bezem & J.F. Groote (Eds.), Typed lambda calculi and applications (pp. 75-90). Berlin Heidelberg: Springer. · Zbl 0795.68127 |
| [7] | Borgo, S., Porello, D., & Troquard, N. (2014). Logical operators for ontological modeling. In P. Garbacz & O. Kutz (Eds.), Formal Ontology in Information Systems: Proceedings of the Eighth International Conference, FOIS 2014, September, 22-25, 2014, Rio de Janeiro, Brazil (pp. 23-36). Amsterdam, The Netherlands: IOS Press |
| [8] | Borgo, S., & Vieu, L. (2009). Artefacts in formal ontology. In A. Meijers (Ed.), Handbook of philosophy of technology and engineering sciences, Handbook of the Philosophy of Science (pp. 273-308). Amsterdam: North-Holland. |
| [9] | Chellas, B. (1969). The logical form of imperatives. Stanford, CA: Perry Lane Press. |
| [10] | Chellas, B. (1980). Modal logic: An introduction. Cambridge: Cambridge University Press. · Zbl 0431.03009 |
| [11] | Chellas, B. (1992). Time and modality in the logic of agency. Studia Logica,51, 485-517. · Zbl 0788.03002 |
| [12] | Courtault, J.-R. & Galmiche, D. (2013). A modal BI logic for dynamic resource properties. In S. Artemov & A. Nerode (Eds.), Logical foundations of computer science (pp. 134-148). Berlin: Springer. · Zbl 1437.03116 |
| [13] | D‘Agostino, M., Gabbay, D. M., & Russo, A. (1997). Grafting modalities onto sub-structural implication systems. Studia Logica,59, 65-102. · Zbl 0888.03011 |
| [14] | De Groote, P. (1996). Partially commutative linear logic: Sequent calculus and phase semantics. In Abrusci & Casadio (Eds.), Third Roma Workshop: Proofs and Linguistics Categories – Applications of Logic to the Analysis and Implementation of Natural Language (pp. 199-208). Bologna: Clueb. |
| [15] | Elgesem, D. (1997). The modal logic of agency. Nordic Journal of Philosophical Logic,2(2), 1-46. · Zbl 0934.03027 |
| [16] | Garbacz, P. (2004). The four dimensions of artifacts. In D. Dubois, C.A. Welty, & M.-A. Williams (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR2004). (pp. 289-299). Palo Alto, CA: AAAI Press. |
| [17] | Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science,50, 1-101. · Zbl 0625.03037 |
| [18] | Girard, J.-Y. (1989). Towards a geometry of interaction. Contemporary Mathematics,92, 69-108. · Zbl 0672.03039 |
| [19] | Governatori, G., & Rotolo, A. (2005). On the axiomatisation of Elgesem’s logic of agency and ability. Journal of Philosophical Logic,34, 403-431. · Zbl 1086.03013 |
| [20] | Harland, J., & Winikoff, M. (2002). Agent negotiation as proof search in linear logic. In C. Castelfranchi & W.L. Johnson (Eds.), Proceedings of the 1st International Joint Conference on Au-tonomous Agents and Multiagent Systems (AAMAS-2002)New York, NY, USA: ACM. · Zbl 1270.68331 |
| [21] | Houkes, W., & Vermaas, P. E. (2010). Technical functions: On the use and design of artefacts. Berlin: Springer. |
| [22] | Kamide, N. (2003). A simplified semantics for a fragment of intuitionistic linear logic. Bulletin of the Section of Logic,32, 123-129. · Zbl 1119.03326 |
| [23] | Kamide, N. (2006). Linear and affine logics with temporal, spatial and epistemic operators. Theoretical Computer Science,353, 165-207. · Zbl 1175.03039 |
| [24] | Kanger, S., & Kanger, H. (1966). Rights and parliamentarism. Theoria,32, 85-115. |
| [25] | Kanovich, M.I., Okada, M. & Terui, K. (2006). Intuitionistic phase semantics is almost classical. Mathematical Structures in Computer Science, 16, 67-86. · Zbl 1095.03071 |
| [26] | Kanovich, M. I., & Vauzeilles, J. (2001). The classical AI planning problems in the mirror of Horn linear logic: Semantics, expressibility, complexity. Mathematical Structures in Computer Science,11, 689-716. · Zbl 0994.68139 |
| [27] | Kroes, P. (2012). Technical artefacts: Creations of mind and matter - A philosophy of engineering design. Berlin: Springer. |
| [28] | Lambek, J. (1958). The mathematics of sentence structure. The American Mathematical Monthly,65, 154-170. · Zbl 0080.00702 |
| [29] | Lincoln, P., Mitchell, J. C., Scedrov, A., & Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic,56, 239-311. · Zbl 0768.03003 |
| [30] | Lismont, L., & Mongin, P. (1994). A non-minimal but very weak axiomatization of common belief. Artificial Intelligence,70, 363-374. · Zbl 0811.03023 |
| [31] | Marion, M., & Sadrzadeh, M. (2004). Reasoning about knowledge in linear logic: Modalities and complexity. In S. Rahman, J. Symons, D. Gabbay, & J. Bendegem (Eds.), Logic, epistemology, and the unity of science (pp. 327-350). Berlin: Springer. · Zbl 1096.03012 |
| [32] | Martens, C., Bosser, A., Ferreira, J.F., & Cavazza, M. (2013). Linear logic programming for narrative generation. In P. Cabalar & T.C. Son (Eds.), Logic Programming and Nonmonotonic Rea-soning, 12th International Conference, LPNMR 2013, Corunna, Spain, September 15-19, 2013, proceedings. (pp. 427-432). Berlin Heidelberg: Springer. |
| [33] | O’Hearn, P. W., & Pym, D. J., (1999). The logic of bunched implications. Bulletin of Symbolic Logic,5, 215-244. · Zbl 0930.03095 |
| [34] | Pauly, M. (2002). A modal logic for coalitional power in games. Journal of Logic and Computation,12, 149-166. · Zbl 1003.91006 |
| [35] | Plotkin, G.D., & Stirling, C. (1986). A framework for intuitionistic modal logics. In J.Y. Halpern (Ed.), Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, Monterey, CA, March 1986 (pp. 399-406). San Francisco, CA, USA: Morgan Kaufmann Publishers Inc. |
| [36] | Porello, D. (2013). A proof-theoretical view of collective rationality. In F. Rossi (Ed.), IJCAI 2013: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013. Palo Alto, CA: {AAAI} Press. |
| [37] | Porello, D., & Endriss, U. (2010a). Modelling combinatorial auctions in linear logic. In F. Lin, U. Sattler & M. Truszczynski (Eds.), Proceedings of the 12th International Conference on the Principles of Knowledge Representation and Reasoning (KR-2010)Palo Alto, CA: AAAI Press. · Zbl 1211.68454 |
| [38] | Porello, D., & Endriss, U. (2010b). Modelling multilateral negotiation in linear logic. In H. Coelho, R. Studer, & M. Wooldridge (Eds.), ECAI 2010: 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, proceedings (pp. 381-386). Amsterdam, The Netherlands: IOS Press. · Zbl 1211.68454 |
| [39] | Porello, D., & Troquard, N. (2014). A resource-sensitive logic of agency. In T. Schaub, G. Friedrich, & B. O’Sullivan (Eds.), ECAI 2014: 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, including Prestigious Applications of Intelligent Systems (PAIS 2014). (pp. 723-728). Amsterdam, The Netherlands: IOS Press. · Zbl 1366.03238 |
| [40] | Pörn, I. (1977). Action theory and social science: Some formal models. Dordrecht: D. Reidel. · Zbl 0371.92027 |
| [41] | Pym, D. J., O’Hearn, P. W., & Yang, H. (2004). Possible worlds and resources: The semantics of BI. Theoretical Computer Science,315, 257-305. · Zbl 1055.03021 |
| [42] | Pym, D. J., & Tofts, C. (2006). A calculus and logic of resources and processes. Formal Aspects of Computing,18, 495-517. · Zbl 1111.68086 |
| [43] | Retoré, C. (1997). Pomset logic: A non-commutative extension of classical linear logic. In P. de Groote & J.R. Hindley (Eds.), Typed lambda calculi and applications (pp. 300-318). Berlin Heidelberg: Springer. · Zbl 1063.03536 |
| [44] | Simpson, A. K. (1994). University of Edinburgh, UK: The proof theory and semantics of intuitionistic modal logic (Unpublished doctoral dissertation). |
| [45] | Troelstra, A. S. (1992). Lectures on linear logic. Stanford, CA: CSLI. · Zbl 0942.03535 |
| [46] | Troquard, N. (2014). Reasoning about coalitional agency and ability in the logics of ’bringing-it-about’. Autonomous Agents and Multi-Agent Systems,28, 381-407. |
| [47] | Urquhart, A. (1972). Semantics for relevant logics. The Journal of Symbolic Logic,37, 159-169. · Zbl 0245.02028 |
| [48] | Vardi, M. Y. (1986). On epistemic logic and logical omniscience. In J.Y. Halpern (Ed.), Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (pp. 293-305). San Francisco, CA, USA: Morgan Kaufmann Publishers Inc. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
