PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 10

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Paraconsistent sequential linear-time temporal logic : combining paraconsistency and sequentiality in temporal reasoning
Kamide N.
Reports on Mathematical Logic
|
2017
|
Vol. 52
3--44
EN
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.
2
Content available remote Interpolation theorems for some variants of LTL
Kamide N.
Reports on Mathematical Logic
|
2015
|
Vol. 50
3--30
EN
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.
3
Content available remote An eight - valued praconsistent logic
Kamide N.
Reports on Mathematical Logic
|
2014
|
Vol. 49
3--21
EN
It is known that many-valued paraconsistent logics are useful for expressing uncertain and inconsistency-tolerant reasoning in a wide range of Computer Science. Some four-valued and sixteen-valued logics have especially been well-studied. Some four-valued logics are not so fine-grained, and some sixteen-valued logics are enough fine-grained, but rather complex. In this paper, a natural eight-valued paraconsistent logic rather than four-valued and sixteen-valued logics is introduced as a Gentzen-type sequent calculus. This eight-valued logic is enough fine-grained and sim- pler than sixteen-valued logic. A triplet valuation semantics is introduced for this logic, and the completeness theorem for this semantics is proved. The cut-elimination theorem for this logic is proved, and this logic is shown to be decidable.
4
Content available remote Reasoning about resources and information : a linear logic approach
Kamide N., Kaneiwa K.
Fundamenta Informaticae
|
2013
|
Vol. 125, nr 1
51--70
EN
A logic called sequence-indexed linear logic (SLL) is proposed to appropriately formalize resource-sensitive reasoning with sequential information. The completeness and cut-elimination theorems for SLL are proved, and SLL and a fragment of SLL are shown to be undecidable and decidable, respectively. As an application of SLL, some specifications of secure password authentication systems are discussed.
5
Content available remote Strong normalization of a typed lambda calculus for intuitionistic bounded linear - time temporal logic
Kamide N.
Reports on Mathematical Logic
|
2012
|
Vol. 47
29--61
EN
Abstract. Linear-time temporal logics (LTLs) are known to be useful for verifying concurrent systems, and a simple natural deduction framework for LTLs has been required to obtain a good computational interpretation. In this paper, a typed A-calculus λAB[l] with a Curry-Howard correspondence is introduced for an in-tuitionistic bounded linear-time temporal logic B[l], of which the time domain is bounded by a fixed positive integer I. The strong normalization theorem for AB[l] is proved as a main result. The base logic B[l] is defined as a Gentzen-type sequent calculus, and despite the restriction on the time domain, B[l] can derive almost all the typical temporal axioms of LTLs. The proposed framework allows us to obtain a uniform and simple proof-theoretical treatment of both natural deduction and sequent calculus, i.e., the equivalence between them, the cut-elimination theorem, the decidability theorem, the Curry-Howard correspondence and the strong normalization theorem can be obtained uniformly.
6
Content available remote A logic of sequences
Kamide N.
Reports on Mathematical Logic
|
2011
|
Vol. 46
29-57
EN
The notion of "sequences" is fundamental to practical reasoning in computer science, because it can appropriately represent "data (information) sequences", "program (execution) sequences", "action sequences", "time sequences","trees", "orders" etc. The aim of this paper is thus to provide a basic logic for reasoning with sequences. A propositional modal logic LS of sequences is introduced as a Gentzen-type sequent calculus by extending Gentzen's LK for classical propositional logic. The completeness theorem with respect to a sequence-indexed semantics for LS is proved, and the cut-elimination theorem for LS is shown. Moreover, a first-order modal logic FLS of sequences, which is a first-order extension of LS, is introduced. The completeness theorem with respect to a first-order sequence-indexed semantics for FLS is proved, and the cut-elimination theorem for FLS is shown. LS and the monadic fragment of FLS are shown to be decidable.
7
Content available remote A Paraconsistent Linear-time Temporal Logic
Kamide N., Wansing H.
Fundamenta Informaticae
|
2011
|
Vol. 106, nr 1
1-23
EN
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.
8
Content available remote Automating and computing paraconsistent reasoning: contraction-free, resolution and type systems
Kamide N.
Reports on Mathematical Logic
|
2010
|
Vol. 45
3-21
EN
Firstly, a contraction-free sequent system G4np for Nelson’s paraconsistent 4-valued logic N4 is introduced by modify- ing and extending a contraction-free system G4ip for intuitionistic propositional logic. The structural rule elimination theorem for G4np can be shown by combining Dyckhoff and Negri’s result for G4ip and an existing embedding result for N4. Secondly, a resolution system Rnp for N4 is introduced by modifying an in- tuitionistic resolution system Rip, which is originally introduced by Mints and modified by Troelstra and Schwichtenberg. The equivalence between Rnp and G4np can be shown. Thirdly, a typed lambda-calculus for N4 is introduced based on Prawitz’s natural deduction system for N4 via the Curry-Howard correspondence. The strong normalization theorem of this calculus can be proved by using Joachimski and Matthes’ proof method for intuitionistic typed lambda-calculi with premutative conversions.
9
Content available remote Foundations of Paraconsistent Resolution
Kamide N.
Fundamenta Informaticae
|
2006
|
Vol. 71, nr 4
419-441
EN
An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic.
10
Content available remote A canonical model construction for substructural logics with strong negation
Kamide N.
Reports on Mathematical Logic
|
2002
|
No. 36
95-116
EN
We introduce Kripke models for propositional substructural logics with strong negation, and show the completeness theorems for these logics using an extended Ishihara's canonical model construction method. The framework presented can deal with a broad range of substructural logics with strong negation, including a modified version of Nelson's logic N$^-$, Wansing's logic COSPL, and extended versions of Visser's basic propositional logic, positive relevant logics, Corsi's logics and M\'endez's logics.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.