Paraconsistent sequential linear-time temporal logic
and its application to medical reasoning
上出哲広

Norihiro Kamide
帝京大学

Inconsistency-tolerant temporal reasoning with sequential (i.e., ordered or hierarchical) information is gaining increasing importance in computer science applications
such as medical informatics and agent communication. A logical system for representing such reasoning is thus required for obtaining a concrete theoretical basis forsuch applications. However, to the best of our knowledge, there are no logical systems
that can simultaneously represent inconsistency, sequentiality, and temporality. Thus,the aim of our study is to introduce a logical system, both semantically and syntactically, for appropriately representing inconsistency-tolerant temporal reasoning withsequential information.
Hence, 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).
Inconsistency-tolerant reasoning in PSLTL is expressed via a paraconsistent negation
connective, and sequential information is represented by sequence modal operators.
Temporal reasoning in PSLTL is, of course, expressed by temporal operators used inLTL. We show that a Kripke-style semantics for PSLTL is useful for appropriately handling medical reasoning in a new model checking framework called paraconsistent modelchecking. We also prove some fundamental theorems for PSLTL, such as completenessand cut-elimination theorems, which are obtained via theorems for semantically andsyntactically embedding PSLTL into its fragments.
The logic PSLTL proposed is regarded as an extension of both LTL and Nelson’s paraconsistent four-valued logic with strong negation N4. On the one hand, LTL is known
to be one of the most useful temporal logics for verifying concurrent systems. On theother hand, N4 is known to be one of the most important base logics for inconsistencytolerant reasoning. The combination of LTL and N4 was previously studied in [3],and such a combined logic was called paraconsistent LTL (PLTL). Combining LTL
with sequence modal operators was also previously studied in [5], and such a combined
logic was called sequence-indexed LTL (SLTL). PSLTL is then obtained from PLTL byadding sequence modal operators, and is also regarded as a modified paraconsistentextension of SLTL. Thus, PSLTL is a modified extension of both PLTL [3] and SLTL
[5].
In the remainder of this abstract, we focus on explanations of an important property of paraconsistent negation and some examples of medical reasoning based on this

property. As mentioned, the paraconsistent negation connective ∼ used in PSLTL cansuitably express inconsistency-tolerant reasoning. One reason why ∼ is considered isthat it can be added in such a way that the extended logic satisfies the property of paraconsistency. A semantic consequence relation |= is called paraconsistent with respect
to a negation connective ∼ if there are formulas α and β such that {α, ∼α} ̸|= β. In
the case of LTL, this implies that there exists a model M and position i of a sequence
σ = t0 , t1 , t2 , ... of time-points in M with (M, i) ̸|= (α ∧ ∼α)→β.
It is known that logical systems with paraconsistency can handle inconsistencytolerant and uncertainty reasoning more appropriately than systems that are nonparaconsistent. We now consider medical reasoning as such reasoning. For example,
we do not want (s(x) ∧ ∼s(x))→d(x) to be satisfied for any symptom s and disease d,
where ∼s(x) means “person x does not have symptom s” and d(x) means “person x
suﬀers from disease d,” because there may be situations that support the truth of boths(a) and ∼s(a) for some individual a but do not support the truth of d(a).
Next, we consider another example.

If we cannot determine whether someone

is healthy, then the vague concept healthy can be represented by asserting the inconsistent formula: healthy(john) ∧ ∼healthy(john).

This is well-formalized inPSLTL because the formula healthy(john) ∧ ∼healthy(john) → hasCancer(john)
where hasCancer(john) means “John has cancer” is not valid in PSLTL (i.e.,
PSLTL is inconsistency-tolerant). On the other hand, the formula healthy(john) ∧¬healthy(john) → hasCancer(john) where ¬ is the classical negation connective isvalid in classical logic (i.e., inconsistency has undesirable consequences). For more
information on paraconsistency and its applications, see e.g., [4, 1] and the references
therein. It is finally remarked that this talk is based on my papers [1, 2].

References[1] N. Kamide, Inconsistency-tolerant temporal reasoning with hierarchical information, Information Sciences 320, pp. 140-155, 2015.
[2] N. Kamide, Inconsistency and sequentiality in LTL, Proceedings of the 7thInternational Conference on Agents and Artificial Intelligence, pp.46-54, 2015.
[3] N. Kamide and H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae 106 (1), pp. 1-23, 2011.
[4] N. Kamide and H. Wansing, Proof theory of Nelson’s paraconsistent logic: A
uniform perspective, Theoretical Computer Science 415, pp. 1-38, 2012.
[5] K. Kaneiwa and N. Kamide, Sequence-indexed linear-time temporal logic: Proofsystem and application, Applied Artificial Intelligence 24, pp. 896-913, 2010.

2