Paraconsistent Sequential Linear-Time Temporal Logic: Combining Paraconsistency and Sequentiality in Temporal Reasoning

Norihiro Kamide


Inconsistency-tolerant temporal reasoning with sequential (i.e., ordered or hierarchical) information is gaining increasing importance in computer science applications. A logical system for representing such reasoning is thus required for obtaining 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 represent inconsistency-tolerant temporal reasoning with sequential information. The cut-elimination, decidability, and completeness theorems for PSLTL are proved in this paper.

Słowa kluczowe: linear-time temporal logic, paraconsistent logic, sequent calculus

[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 inconsistent 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, AddisonWesley, 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 eEducation, 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¨ur 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. 

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.