Paraconsistent sequential linear-time temporal logic : combining paraconsistency and sequentiality in temporal reasoning

• Autorzy: Kamide N.

Identyfikatory

DOI

10.4467/20842589RM.17.001.7139

• Języki publikacji: EN

Abstrakty

EN

Inconsistency-tolerant temporal reasoning with sequential (i.e., ordered or hierarchical) information is gaining in- creasing importance in computer science applications. A logical system for representing such reasoning is thus required for ob- taining a theoretical basis for such applications. In this paper, we introduce a new logic called paraconsistent sequential linear-time temporal logic (PSLTL), which is an extension of the standard linear-time temporal logic (LTL). PSLTL can appropriately rep- resent inconsistency-tolerant temporal reasoning with sequential information. The cut-elimination, decidability, and completeness theorems for PSLTL are proved in this paper.

Słowa kluczowe

EN

linear-time temporal logic; paraconsistent logic; sequent calculus

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2017
• Tom: Vol. 52
• Strony: 3--44
• Opis fizyczny: Bibliogr. 32 poz.

Twórcy

autor

Kamide N.

• Teikyo University, Faculty of Science and Engineering Department of Information and Electronic Engineering Toyosatodai 1-1, Utsunomiya Tochigi 320-8551, Japan

Bibliografia

• [1] A. Almukdad and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1984), 231-233.
• [2] O. Arieli and A. Zamansky, A framework for reasoning under uncertainty based on non-deterministic distance semantics, International Journal of Approximate Reasoning 52:2 (2011), 184-211.
• [3] S. Baratella and A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic 43 (2004), 965-990.
• [4] D. Chen and J.Wu, Reasoning about inconsistent concurrent systems: A non-classical temporal logic, Proceedings of the 32nd Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2006), Lecture Notes in Computer Science 3831, pp. 207-217, 2006.
• [5] E.M. Clarke and E.A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Lecture Notes in Computer Science 131 (1981), 52-71.
• [6] E.M. Clarke, O. Grumberg, and D.A. Peled, Model checking, The MIT Press, 1999.
• [7] S. Easterbrook, and M. Chechik, A framework for multi-valued reasoning over in-consistent viewpoints, Proceedings of the 23rd International Conference on Software Engineering (ICSE 2001), pp. 411-420, 2001.
• [8] E.A. Emerson, Temporal and modal logic, In: Handbook of Theoretical Computer Science, Formal Models and Semantics (B), Jan van Leeuwen (Ed.), pp. 995-1072, Elsevier and MIT Press, 1990.
• [9] D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM Symposium on Principles of Programming Languages, ACM Press, pp. 163-173, 1980.
• [10] Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36 (1977), 49-59.
• [11] G.J. Holzmann, The SPIN model checker: Primer and reference manual, Addison-Wesley, 2006.
• [12] N. Kamide, An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of the Logic 35:4 (2006), 187-194.
• [13] N. Kamide, Extended full computation tree logics for paraconsistent model checking, Logic and Logical Philosophy 15:3 (2006), 251-276.
• [14] N. Kamide, 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, pp. 283-292, 2010.
• [15] N. Kamide, An extended LTL for inconsistency-tolerant reasoning with hierarchical information: Verifying students' learning processes, International Journal of e-Education, e-Business, e-Management and e-Learning 3 (3), pp. 234-238, IACSIT Press, 2013.
• [16] N. Kamide, Modeling and verifying inconsistency-tolerant temporal reasoning with hierarchical information: Dealing with students' learning processes, Proceedings of the 2013 IEEE International Conference on Systems, Man, and Cybernetics (IEEE SMC 2013), pp. 1859-1864, 2013.
• [17] N. Kamide, Inconsistency and sequentiality in LTL, Proceedings of the 7th International Conference on Agents and Artificial Intelligence (ICAART 2015), pp. 46-54,2015.
• [18] N. Kamide, Inconsistency-tolerant temporal reasoning with hierarchical information, Information Sciences 320 (2015), 140-155.
• [19] N. Kamide and K. Kaneiwa, Extended full computation-tree logic with sequence modal operator: representing hierarchical tree structures, Proceedings of the 22nd Australasian Joint Conference on Artificial Intelligence, Lecture Notes in Artificial Intelligence 5866, pp. 485-494, 2009.
• [20] N. Kamide and K. Kaneiwa, Paraconsistent negation and classical negation in computation tree logic, Proceedings of the 2nd International Conference on Agents and Artificial Intelligence (ICAART 2010), Vol. 1, pp. 464-469, 2010.
• [21] N. Kamide and H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae 106:1 (2011), 1-23.
• [22] N. Kamide and H.Wansing, Proof theory of Nelson's paraconsistent logic: A uniform perspective, Theoretical Computer Science 415 (2012), 1-38.
• [23] K. Kaneiwa and N. Kamide, Sequence-indexed linear-time temporal logic: Proof system and application, Applied Artificial Intelligence 24 (2010), 896-913.
• [24] K. Kaneiwa and N. Kamide, Paraconsistent computation tree logic, New Generation Computing 29:4 (2011), 391-408.
• [25] K. Kaneiwa and N. Kamide, Conceptual modeling in full computation-tree logic with sequence modal operator, International Journal of Intelligent Systems 26:7 (2011), 636-651.
• [26] H. Kawai, Sequential calculus for a first order infinitary temporal logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33 (1987), 423-432.
• [27] D. Nelson, Constructible falsity, Journal of Symbolic Logic 14 (1949), 16-26.
• [28] A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46-57, 1977.
• [29] G. Priest, Paraconsistent logic, Handbook of Philosophical Logic (Second Edition), Vol. 6, D. Gabbay and F. Guenthner (eds.), Kluwer Academic Publishers, Dordrecht,pp. 287-393, 2002.
• [30] W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg, Braunschweig, 1979.
• [31] N. Vorob'ev, A constructive propositional logic with strong negation, Doklady Akademii Nauk SSSR 85 (1952), 465-468, (in Russian).
• [32] H. Wansing, The logic of information structures, Lecture Notes in Artificial Intelligence 681, 163 pages, 1993.

Uwagi

PL

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).