Reasoning about resources and information : a linear logic approach

• Autorzy: Kamide N. , Kaneiwa K.
• Języki publikacji: EN

Abstrakty

EN

A logic called sequence-indexed linear logic (SLL) is proposed to appropriately formalize resource-sensitive reasoning with sequential information. The completeness and cut-elimination theorems for SLL are proved, and SLL and a fragment of SLL are shown to be undecidable and decidable, respectively. As an application of SLL, some specifications of secure password authentication systems are discussed.

Słowa kluczowe

EN

completeness theorem; informational interpretation; linear logic; resource-sensitive reasoning; secure password authentication system; sequence modal operator

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 125, nr 1
• Strony: 51--70
• Opis fizyczny: Bibliogr. 15 poz.

Twórcy

autor

Kamide N.

• Faculty of Information Technology and Business, Cyber University, Japan Cyber Educational Institute, Ltd., 4F of Izumi Shiba-kouen Building, 1-6-8 Shiba-kouen, Minato-ku, Tokyo 105-0011, Japan

autor

Kaneiwa K.

• Department of Electrical Engineering and Computer Science, Iwate University, 4-3-5 Ueda, Morioka, Iwate 020-8551, Japan

Bibliografia

• [1] Girard, J.-Y.: Linear logic, Theoretical Computer Science 50, 1987, 1-102.
• [2] Kamide, N.: Combining soft linear logic and spatio-temporal operators, Journal of Logic and Computation 14 (5), 2004, 625-650.
• [3] Kamide, N.: Linear and affine logics with temporal, spatial and epistemic operators, Theoretical Computer Science 353 (1-3), 2006, 165-207.
• [4] Kamide, N.: A proof system for temporal reasoning with sequential information, Proceedings of the 20th Brazilian Symposium on Artificial Intelligence (SBIA 2010), Lecture Notes in Artificial Intelligence 6404, Springer, 2010, 283-292.
• [5] Kamide, N. and Kaneiwa, K.: Extended full computation-tree logic with sequence modal operator: Representing hierarchical tree structures, Proceedings of the 22nd Australasian Joint Conference on Artificial Intelligence (AI’09), Lecture Notes in Artificial Intelligence 5866, 2009, 485-494.
• [6] Kamide, N. and Kaneiwa, K.: Resource-sensitive reasoning with sequential information, Proceedings of the 23rd Australasian Joint Conference on Artificial Intelligence (AI’10), Lecture Notes in Artificial Intelligence, 6464,2010, 22-31.
• [7] Kaneiwa, K.: Order-sorted logic programming with predicate hierarchy, Artificial Intelligence 158 (2), 2004, 155-188.
• [8] Kaneiwa, K. and Kamide, N.: Sequence-indexed linear-time temporal logic: Proof system and application, Applied Artificial Intelligence 24 (10), 2010, 896-913.
• [9] Kaneiwa, K. and Nguyen, H. P.: An Order-Sorted Query System for Sort, Predicate, and Meta-Predicate Hierarchies, Knowledge and Information Systems, Springer, 2012, published online.
• [10] Lincoln, P., Mitchell, J.C., Scedrov, A. and Shankar, N.: Decision problems for propositional linear logic, Annals of Pure and Applied Logic 56, 1992, 239-311.
• [11] Miller, D.: An overview of linear logic programming, in: London Mathematical Society Lecture Note Series 316 (Linear logic in computer science) (T. Ehrhard, J.-Y. Girard, P. Ruet and P. Scott Eds.), Cambridge University Press, 2004, 119-150.
• [12] Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science 281, 2002,471-498.
• [13] Pym, D.J., O’Hearn, P.W. and Yang, H.: Possible worlds and resources: The semantics of BI, Theoretical Computer Science 315, 2004, 257-305.
• [14] Russell, S. and Norvig, P.: Artificial intelligence: A modern approach (Second edition), Pearson Education, Inc., 2003.
• [15] Wansing, H.: The logic of information structures, Lecture Notes in Artificial Intelligence 681, 1993, 1-163.