Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: cut-elimination

Sortuj według:

Ogranicz wyniki do:

A semantical analysis of cut-free calculi for modal logics

Takano M.

Reports on Mathematical Logic

2018

Vol. 53

43--65

We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics which are obtained from the least normal logic K by adding axioms from T, 4, 5, D and B. This implies Kripke completeness, as well as the cutelimination property or the subformula property of the calculi. By slightly modifying the arguments, the finite model property of the logics also follows.

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.

An Infinitary Sequent System for the Equational Theory of *-continuous Action Lattices

Palka E.

Fundamenta Informaticae

2007

Vol. 78, nr 2

295-309

We present an infinitary logic ACTw in the form of a Gentzen-style sequent system, which is equivalent to the equational theory of *-continuous action lattices [9]. We prove the cut-elimination theorem for ACTw and, as a consequence, a theorem on the elimination of negative occurrences of *. This shows that ACTw is P01, whence, by a result of Buszkowski [1], it is P01-complete.