Annotated Evidential Linear-time Temporal Logic

Existing linear-time temporal logic LTL is based on classical bivalent logic, so it is insufficient to handle inconsistent situations such as contradicted phenomena. The annotated evidential logic is the family of paraconsistent annotated logic based on beliefs and disbeliefs and allows for a more fine-grained understanding of the situation. In this research, we propose annotated evidential linear-time temporal logic ELTLτ and its deductive system with tableau calculus. We provide examples of tableau proof and a sketch of the completeness theorem.