Affiliations: Waseda Institute for Advanced Study, 1-6-1 Nishi Waseda, Shinjuku-ku, Tokyo 169-8050, Japan. [email protected] | Ruhr-Universität Bochum, Department of Philosophy II, Carnap Institute for Philosophy and Science, Universitätsstr. 150, 44780 Bochum, Germany. [email protected]
Note: [] Address for correspondence: Waseda Institute for Advanced Study, 1-6-1 NishiWaseda, Shinjuku-ku, Tokyo 169-8050, Japan
Abstract: Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time temporal logic (PLTL), is obtained semantically from the linear-time temporal logic LTL by adding a paraconsistent negation. Some theorems for embedding PLTL into LTL are proved, and PLTL is shown to be decidable. A Gentzentype sequent calculus PLTω for PLTL is introduced, and the completeness and cut-elimination theorems for this calculus are proved. In addition, a display calculus δPLTω for PLTL is defined.
