Modeling and Verifying Inconsistency-Tolerant Temporal Reasoning with Hierarchical Information: Dealing with Students´ Learning Processes

In this paper, we propose a formal method for modeling and verifying inconsistency-tolerant temporal reasoning with hierarchical information. For this purpose, a temporal logic called sequential paraconsistent computation tree logic (SPCTL) is obtained from the well-known computation tree logic (CTL) by adding a paraconsistent negation connective and some sequence modal operators. SPCTL can appropriately represent both, inconsistency-tolerant reasoning by the paraconsistent negation connective, and hierarchical information by the sequence modal operators. The validity, satisfiability and model-checking problems of SPCTL are shown to be EXPTIME-complete, deterministic EXPTIME-complete and deterministic PTIME-complete, respectively. Some new illustrative examples for students´ learning processes are presented using SPCTL.