Affiliations: 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. drnkamide08@kpd.biglobe.ne.jp | Department of Electrical Engineering and Computer Science, Iwate University, 4-3-5 Ueda, Morioka, Iwate 020-8551, Japan. kaneiwa@cis.iwate-u.ac.jp
Note: [] Address for correspondence: 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
Abstract: 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.
Keywords: Linear logic, resource-sensitive reasoning, sequence modal operator, informational interpretation, completeness theorem, secure password authentication system
