Order:
Disambiguations
Norihiro Kamide [68]N. Kamide [2]Norihori Kamide [1]
  1.  28
    Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic.Norihiro Kamide - 2023 - Studia Logica 111 (6):979-1014.
    This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  2.  38
    Proof Theory of Paraconsistent Quantum Logic.Norihiro Kamide - 2018 - Journal of Philosophical Logic 47 (2):301-324.
    Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  3.  27
    Modal Multilattice Logic.Norihiro Kamide & Yaroslav Shramko - 2017 - Logica Universalis 11 (3):317-343.
    A modal extension of multilattice logic, called modal multilattice logic, is introduced as a Gentzen-type sequent calculus \. Theorems for embedding \ into a Gentzen-type sequent calculus S4C and vice versa are proved. The cut-elimination theorem for \ is shown. A Kripke semantics for \ is introduced, and the completeness theorem with respect to this semantics is proved. Moreover, the duality principle is proved as a characteristic property of \.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  4.  31
    Falsification-Aware Semantics and Sequent Calculi for Classical Logic.Norihiro Kamide - 2021 - Journal of Philosophical Logic 51 (1):99-126.
    In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic. In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3. The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schütte’s method. Similar results for the propositional case are also obtained.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  5.  34
    Lattice Logic, Bilattice Logic and Paraconsistent Quantum Logic: a Unified Framework Based on Monosequent Systems.Norihiro Kamide - 2021 - Journal of Philosophical Logic 50 (4):781-811.
    Lattice logic, bilattice logic, and paraconsistent quantum logic are investigated based on monosequent systems. Paraconsistent quantum logic is an extension of lattice logic, and bilattice logic is an extension of paraconsistent quantum logic. Monosequent system is a sequent calculus based on the restricted sequent that contains exactly one formula in both the antecedent and succedent. It is known that a completeness theorem with respect to a lattice-valued semantics holds for a monosequent system for lattice logic. A completeness theorem with respect (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  37
    Paraconsistent Double Negations as Classical and Intuitionistic Negations.Norihiro Kamide - 2017 - Studia Logica 105 (6):1167-1191.
    A classical paraconsistent logic, which is regarded as a modified extension of first-degree entailment logic, is introduced as a Gentzen-type sequent calculus. This logic can simulate the classical negation in classical logic by paraconsistent double negation in CP. Theorems for syntactically and semantically embedding CP into a Gentzen-type sequent calculus LK for classical logic and vice versa are proved. The cut-elimination and completeness theorems for CP are also shown using these embedding theorems. Similar results are also obtained for an intuitionistic (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  7.  43
    Kripke Completeness of Bi-intuitionistic Multilattice Logic and its Connexive Variant.Norihiro Kamide, Yaroslav Shramko & Heinrich Wansing - 2017 - Studia Logica 105 (6):1193-1219.
    In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  8.  20
    Falsification-Aware Calculi and Semantics for Normal Modal Logics Including S4 and S5.Norihiro Kamide - 2023 - Journal of Logic, Language and Information 32 (3):395-440.
    Falsification-aware (hyper)sequent calculi and Kripke semantics for normal modal logics including S4 and S5 are introduced and investigated in this study. These calculi and semantics are constructed based on the idea of a falsification-aware framework for Nelson’s constructive three-valued logic. The cut-elimination and completeness theorems for the proposed calculi and semantics are proved.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  22
    Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - 2020 - Journal of Philosophical Logic 49 (6):1185-1212.
    Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  10.  10
    Alternative Multilattice Logics: An Approach Based on Monosequent and Indexed Monosequent Calculi.Norihiro Kamide - 2021 - Studia Logica 109 (6):1241-1271.
    Two new multilattice logics called submultilattice logic and indexed multilattice logic are introduced as a monosequent calculus and an indexed monosequent calculus, respectively. The submultilattice logic is regarded as a monosequent calculus version of Shramko’s original multilattice logic, which is also known as the logic of logical multilattices. The indexed multilattice logic is an extension of the submultilattice logic, and is regarded as the logic of multilattices. A completeness theorem with respect to a lattice-valued semantics is proved for the submultilattice (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  28
    Modal and Intuitionistic Variants of Extended Belnap–Dunn Logic with Classical Negation.Norihiro Kamide - 2021 - Journal of Logic, Language and Information 30 (3):491-531.
    In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  12.  82
    Sequent calculi for some trilattice logics.Norihiro Kamide & Heinrich Wansing - 2009 - Review of Symbolic Logic 2 (2):374-395.
    The trilattice SIXTEEN3 introduced in Shramko & Wansing (2005) is a natural generalization of the famous bilattice FOUR2. Some Hilbert-style proof systems for trilattice logics related to SIXTEEN3 have recently been studied (Odintsov, 2009; Shramko & Wansing, 2005). In this paper, three sequent calculi GB, FB, and QB are presented for Odintsovs coordinate valuations associated with valuations in SIXTEEN3. The equivalence between GB, FB, and QB, the cut-elimination theorems for these calculi, and the decidability of B are proved. In addition, (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  13.  26
    Combining linear-time temporal logic with constructiveness and paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
  14.  19
    Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework.Norihiro Kamide - 2019 - Logica Universalis 13 (1):37-63.
    Gentzen-type sequent calculi GBD+, GBDe, GBD1, and GBD2 are respectively introduced for De and Omori’s axiomatic extensions BD+, BDe, BD1, and BD2 of Belnap–Dunn logic by adding classical negation. These calculi are constructed based on a small modification of the original characteristic axiom scheme for negated implication. Theorems for syntactically and semantically embedding these calculi into a Gentzen-type sequent calculus LK for classical logic are proved. The cut-elimination, decidability, and completeness theorems for these calculi are obtained using these embedding theorems. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  15.  21
    Sequent Calculi for Intuitionistic Linear Logic with Strong Negation.Norihiro Kamide - 2002 - Logic Journal of the IGPL 10 (6):653-678.
    We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third one is called a triple-context calculus, which is regarded as a natural (...)
    Direct download  
     
    Export citation  
     
    Bookmark   11 citations  
  16.  33
    Quantized linear logic, involutive quantales and strong negation.Norihiro Kamide - 2004 - Studia Logica 77 (3):355-384.
    A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  17.  37
    A note on dual-intuitionistic logic.Norihiro Kamide - 2003 - Mathematical Logic Quarterly 49 (5):519.
    Dual-intuitionistic logics are logics proposed by Czermak , Goodman and Urbas . It is shown in this paper that there is a correspondence between Goodman's dual-intuitionistic logic and Nelson's constructive logic N−.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  18.  18
    Modal extension of ideal paraconsistent four-valued logic and its subsystem.Norihiro Kamide & Yoni Zohar - 2020 - Annals of Pure and Applied Logic 171 (10):102830.
    This study aims to introduce a modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC as a Gentzen-type sequent calculus and prove the Kripke-completeness and cut-elimination theorems for M4CC. The logic M4CC is also shown to be decidable and embeddable into the normal modal logic S4. Furthermore, a subsystem of M4CC, which has some characteristic properties that do not hold for M4CC, is introduced and the Kripke-completeness and cut-elimination theorems for this subsystem are proved. This subsystem (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  19. A Canonical Model Construction For Substructural Logics With Strong Negation.N. Kamide - 2002 - Reports on Mathematical Logic:95-116.
    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.
     
    Export citation  
     
    Bookmark   9 citations  
  20.  39
    Gentzen-Type Methods for Bilattice Negation.Norihiro Kamide - 2005 - Studia Logica 80 (2-3):265-289.
    A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  21. Kripke semantics for modal substructural logics.Norihiro Kamide - 2002 - Journal of Logic, Language and Information 11 (4):453-470.
    We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  22.  37
    A Hierarchy of Weak Double Negations.Norihiro Kamide - 2013 - Studia Logica 101 (6):1277-1297.
    In this paper, a way of constructing many-valued paraconsistent logics with weak double negation axioms is proposed. A hierarchy of weak double negation axioms is addressed in this way. The many-valued paraconsistent logics constructed are defined as Gentzen-type sequent calculi. The completeness and cut-elimination theorems for these logics are proved in a uniform way. The logics constructed are also shown to be decidable.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  23.  45
    An embedding-based completeness proof for Nelson's paraconsistent logic.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (3/4):205-214.
  24.  50
    A relationship between Rauszer's HB logic and Nelson's logic'.Norihiro Kamide - 2004 - Bulletin of the Section of Logic 33 (4):237-249.
  25.  50
    Substructural logics with Mingle.Norihiro Kamide - 2002 - Journal of Logic, Language and Information 11 (2):227-249.
    We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FLm (full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm (Lambek calculuswith restricted mingle).
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  26.  15
    Extending paraconsistent quantum logic: a single-antecedent/succedent system approach.Norihiro Kamide - 2018 - Mathematical Logic Quarterly 64 (4-5):371-386.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  27.  23
    A cut-free system for 16-valued reasoning.Norihiro Kamide - 2005 - Bulletin of the Section of Logic 34 (4):213-226.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  28.  51
    Natural deduction systems for Nelson's paraconsistent logic and its neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
    Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a sublogic of N4. Fifthly, a strong normalization theorem is (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  29. Benevides, MRF, 343 Berk, L., 323 Boėr, SE, 43 Calabrese, PG.S. Chopra, A. G. Cohn, R. P. de Freitas, H. Field, A. Ghose, L. Goble, V. Halbach, L. Humberstone, N. Kamide & S. Kovac - 2003 - Journal of Philosophical Logic 32 (669).
    No categories
     
    Export citation  
     
    Bookmark   5 citations  
  30.  22
    Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.Norihiro Kamide & Yoni Zohar - 2020 - Studia Logica 108 (3):549-571.
    In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  71
    Substructural implicational logics including the relevant logic E.Ryo Kashima & Norihiro Kamide - 1999 - Studia Logica 63 (2):181-212.
    We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  32.  16
    Symmetric and conflated intuitionistic logics.Norihiro Kamide - forthcoming - Logic Journal of the IGPL.
    Two new propositional non-classical logics, referred to as symmetric intuitionistic logic (SIL) and conflated intuitionistic logic (CIL), are introduced as indexed and non-indexed Gentzen-style sequent calculi. SIL is regarded as a natural hybrid logic combining intuitionistic and dual-intuitionistic logics, whereas CIL is regarded as a variant of intuitionistic paraconsistent logic with conflation and without paraconsistent negation. The cut-elimination theorems for SIL and CIL are proved. CIL is shown to be conservative over SIL.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33.  45
    Phase semantics and Petri net interpretation for resource-sensitive strong negation.Norihiro Kamide - 2006 - Journal of Logic, Language and Information 15 (4):371-401.
    Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  34.  9
    Rules of Explosion and Excluded Middle: Constructing a Unified Single-Succedent Gentzen-Style Framework for Classical, Paradefinite, Paraconsistent, and Paracomplete Logics.Norihiro Kamide - forthcoming - Journal of Logic, Language and Information:1-36.
    A unified and modular falsification-aware single-succedent Gentzen-style framework is introduced for classical, paradefinite, paraconsistent, and paracomplete logics. This framework is composed of two special inference rules, referred to as the rules of explosion and excluded middle, which correspond to the principle of explosion and the law of excluded middle, respectively. Similar to the cut rule in Gentzen’s LK for classical logic, these rules are admissible in cut-free LK. A falsification-aware single-succedent Gentzen-style sequent calculus fsCL for classical logic is formalized based (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  35.  27
    Proof Systems Combining Classical and Paraconsistent Negations.Norihiro Kamide - 2009 - Studia Logica 91 (2):217-238.
    New propositional and first-order paraconsistent logics (called L ω and FL ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L ω and FL ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L ω and FL ω are proved. The cut-elimination theorems for L ω and FL ω are shown using both syntactical ways via the embedding theorems and semantical ways (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  36.  19
    Completeness and cut-elimination theorems for trilattice logics.Norihiro Kamide & Heinrich Wansing - 2011 - Annals of Pure and Applied Logic 162 (10):816-835.
    A sequent calculus for Odintsov’s Hilbert-style axiomatization of a logic related to the trilattice SIXTEEN3 of generalized truth values is introduced. The completeness theorem w.r.t. a simple semantics for is proved using Maehara’s decomposition method that simultaneously derives the cut-elimination theorem for . A first-order extension of and its semantics are also introduced. The completeness and cut-elimination theorems for are proved using Schütte’s method.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  37.  29
    Notes on Craig interpolation for LJ with strong negation.Norihiro Kamide - 2011 - Mathematical Logic Quarterly 57 (4):395-399.
    The Craig interpolation theorem is shown for an extended LJ with strong negation. A new simple proof of this theorem is obtained. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  38.  52
    Normal modal substructural logics with strong negation.Norihiro Kamide - 2003 - Journal of Philosophical Logic 32 (6):589-612.
    We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  39.  27
    Paraconsistent double negation as a modal operator.Norihiro Kamide - 2016 - Mathematical Logic Quarterly 62 (6):552-562.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  40. Natural deduction systems for some non-commutative logics.Norihiro Kamide & Motohiko Mouri - 2007 - Logic and Logical Philosophy 16 (2-3):105-146.
    Varieties of natural deduction systems are introduced for Wansing’s paraconsistent non-commutative substructural logic, called a constructive sequential propositional logic (COSPL), and its fragments. Normalization, strong normalization and Church-Rosser theorems are proved for these systems. These results include some new results on full Lambek logic (FL) and its fragments, because FL is a fragment of COSPL.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  41.  21
    Synthesized substructural logics.Norihiro Kamide - 2007 - Mathematical Logic Quarterly 53 (3):219-225.
    A mechanism for combining any two substructural logics (e.g. linear and intuitionistic logics) is studied from a proof-theoretic point of view. The main results presented are cut-elimination and simulation results for these combined logics called synthesized substructural logics.
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  42. Temporal non-commutative logic: Expressing time, resource, order and hierarchy.Norihiro Kamide - 2009 - Logic and Logical Philosophy 18 (2):97-126.
    A first-order temporal non-commutative logic TN[l], which has no structural rules and has some l-bounded linear-time temporal operators, is introduced as a Gentzen-type sequent calculus. The logic TN[l] allows us to provide not only time-dependent, resource-sensitive, ordered, but also hierarchical reasoning. Decidability, cut-elimination and completeness (w.r.t. phase semantics) theorems are shown for TN[l]. An advantage of TN[l] is its decidability, because the standard first-order linear-time temporal logic is undecidable. A correspondence theorem between TN[l] and a resource indexed non-commutative logic RN[l] (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  43.  18
    Bounded linear-time temporal logic: A proof-theoretic investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
  44.  20
    An Extended Paradefinite Logic Combining Conflation, Paraconsistent Negation, Classical Negation, and Classical Implication: How to Construct Nice Gentzen-type Sequent Calculi.Norihiro Kamide - 2022 - Logica Universalis 16 (3):389-417.
    In this study, an extended paradefinite logic with classical negation (EPLC), which has the connectives of conflation, paraconsistent negation, classical negation, and classical implication, is introduced as a Gentzen-type sequent calculus. The logic EPLC is regarded as a modification of Arieli, Avron, and Zamansky’s ideal four-valued paradefinite logic (4CC) and as an extension of De and Omori’s extended Belnap–Dunn logic with classical negation (BD+) and Avron’s self-extensional four-valued paradefinite logic (SE4). The completeness, cut-elimination, and decidability theorems for EPLC are proved (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45. Automating and computing paraconsistent reasoning: contraction-free, resolution and type systems.Norihiro Kamide - 2010 - Reports on Mathematical Logic:3-21.
     
    Export citation  
     
    Bookmark   1 citation  
  46.  14
    A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics.Norihiro Kamide - 2016 - Mathematical Logic Quarterly 62 (3):177-189.
    In this paper, the positive fragment of the logic math formula of contraction-less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four-valued logic math formula. This extended relevant logic is called math formula, and it has the property of constructible falsity which is known to be a characteristic property of math formula. A Gentzen-type sequent calculus math formula for math formula is introduced, and the cut-elimination and decidability (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  47. A Logic Of Sequences.Norihiro Kamide - 2011 - Reports on Mathematical Logic:29-57.
     
    Export citation  
     
    Bookmark  
  48.  23
    A note on Decision problems for Implicational Sequent Calculi.Norihiro Kamide - 2001 - Bulletin of the Section of Logic 30 (3):129-138.
  49.  20
    A spatial modal logic with a location interpretation.Norihiro Kamide - 2005 - Mathematical Logic Quarterly 51 (4):331.
    A spatial modal logic is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut-elimination theorem for a modified subsystem of SML are also presented.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  50.  7
    Bunched sequential information.Norihiro Kamide - 2016 - Journal of Applied Logic 15:150-170.
1 — 50 / 70