Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: linear-time temporal logic

Sortuj według:

Ogranicz wyniki do:

Paraconsistent sequential linear-time temporal logic : combining paraconsistency and sequentiality in temporal reasoning

Kamide N.

Reports on Mathematical Logic

2017

Vol. 52

3--44

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

Interpolation theorems for some variants of LTL

Kamide N.

Reports on Mathematical Logic

2015

Vol. 50

3--30

It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theorems are shown for some fragments and extensions of LTL. These theorems are simply proved based on an embedding-based proof method with Gentzen-type sequent calculi. Maksimova separation theorems (Maksimova principle of variable separation) are also shown for these LTL variants.

A Paraconsistent Linear-time Temporal Logic

Kamide N., Wansing H.

Fundamenta Informaticae

2011

Vol. 106, nr 1

1-23

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.