54 found
Order:
  1.  3
    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   2 citations  
  2.  8
    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   2 citations  
  3. 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 (7 more)  
     
    Export citation  
     
    Bookmark  
  4. 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 (7 more)  
     
    Export citation  
     
    Bookmark  
  5.  7
    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   1 citation  
  6.  17
    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 (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  7.  4
    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   1 citation  
  8.  5
    Combining Linear-Time Temporal Logic with Constructiveness and Paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
  9.  32
    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   5 citations  
  10.  16
    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   3 citations  
  11.  4
    Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework.Norihiro Kamide - forthcoming - Logica Universalis:1-27.
    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  
  12.  5
    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 (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  13.  7
    A Relationship Between Rauszer's HB Logic and Nelson's Logic'.Norihiro Kamide - 2004 - Bulletin of the Section of Logic 33 (4):237-249.
  14.  13
    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 (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  15.  22
    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 (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  16.  4
    Paraconsistent Double Negation as a Modal Operator.Norihiro Kamide - 2016 - Mathematical Logic Quarterly 62 (6):552-562.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  17.  8
    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   4 citations  
  18.  65
    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 (7 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  19.  24
    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 (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  20.  26
    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 (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  21.  2
    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 (2 more)  
     
    Export citation  
     
    Bookmark  
  22.  26
    An Embedding-Based Completeness Proof for Nelson's Paraconsistent Logic.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (3/4):205-214.
  23.  5
    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 (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24.  10
    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 (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  25
    Dynamic Non-Commutative Logic.Norihiro Kamide - 2010 - Journal of Logic, Language and Information 19 (1):33-51.
    A first-order dynamic non-commutative logic, which has no structural rules and has some program operators, is introduced as a Gentzen-type sequent calculus. Decidability, cut-elimination and completeness theorems are shown for DN or its fragments. DN is intended to represent not only program-based, resource-sensitive, ordered, sequence-based, but also hierarchical reasoning.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  26.  30
    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 (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  27.  8
    Symmetric and Dual Paraconsistent Logics.Norihiro Kamide & Heinrich Wansing - 2010 - Logic and Logical Philosophy 19 (1-2):7-30.
    Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL are introduced, and the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  28.  1
    Phase Semantics for Linear-Time Formalism.Norihiro Kamide - 2011 - Logic Journal of the IGPL 19 (1):121-143.
    It is known that linear-time temporal logic is a useful logic for verifying and specifying concurrent systems. In this paper, phase semantics for LTL and its substructural refinements is introduced, and the completeness and cut-elimination theorems for LTL and its refinements are proved based on this semantics.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  29.  15
    Natural Deduction Systems for Nelson's Paraconsistent Logic and its Neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
  30.  26
    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 (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  11
    A Note on Decision Problems for Implicational Sequent Calculi.Norihiro Kamide - 2001 - Bulletin of the Section of Logic 30 (3):129-138.
  32.  24
    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 (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33. Combining Intuitionistic Logic with Paraconsistent Operators.Norihiro Kamide - 2012 - Logique Et Analyse 217:57-71.
  34.  19
    Temporalizing Linear Logic.Norihiro Kamide - 2007 - Bulletin of the Section of Logic 36 (3/4):173-182.
    Direct download  
     
    Export citation  
     
    Bookmark  
  35.  14
    Cut-Free Single-Succedent Systems Revisited.Norihiro Kamide - 2005 - Bulletin of the Section of Logic 34 (3):165-175.
    Direct download  
     
    Export citation  
     
    Bookmark  
  36.  23
    Synchronized Linear-Time Temporal Logic.Heinrich Wansing & Norihiro Kamide - 2011 - Studia Logica 99 (1-3):365-388.
    A new combined temporal logic called synchronized linear-time temporal logic (SLTL) is introduced as a Gentzen-type sequent calculus. SLTL can represent the n -Cartesian product of the set of natural numbers. The cut-elimination and completeness theorems for SLTL are proved. Moreover, a display sequent calculus δ SLTL is defined.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  37.  13
    Strong Normalization of Program-Indexed Lambda Calculus.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (1/2):65-78.
    Direct download  
     
    Export citation  
     
    Bookmark  
  38.  12
    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  
  39.  11
    Extended Full Computation-Tree Logics for Paraconsistent Model Checking.Norihiro Kamide - 2007 - Logic and Logical Philosophy 15 (3):251-276.
    It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  40.  7
    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 (3 more)  
     
    Export citation  
     
    Bookmark  
  41.  20
    Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
    The strong normalization theorem is uniformly proved for typed λ-calculi for a wide range of substructural logics with or without strong negation.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  42.  2
    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 (3 more)  
     
    Export citation  
     
    Bookmark  
  43.  7
    Bounded Linear-Time Temporal Logic: A Proof-Theoretic Investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
  44.  4
    Towards a Theory of Resource: An Approach Based on Soft Exponentials.Norihiro Kamide - 2007 - Journal of Applied Non-Classical Logics 17 (1):63-89.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45.  4
    On a Logic of Involutive Quantales.Norihiro Kamide - 2005 - Mathematical Logic Quarterly 51 (6):579-585.
    The logic just corresponding to involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut-free sequent calculus formulation, and the completeness theorem for this logic is proved using a new admissible rule.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  46.  3
    Temporal Gödel-Gentzen and Girard Translations.Norihiro Kamide - 2013 - Mathematical Logic Quarterly 59 (1-2):66-83.
    A theorem for embedding a first-order linear- time temporal logic LTL into its intuitionistic counterpart ILTL is proved using Baratella-Masini's temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic. A substructural counterpart LLTL of ILTL is introduced, and a theorem for embedding ILTL into LLTL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic. These embedding theorems are proved syntactically based on Gentzen-type sequent calculi.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  47.  2
    Representing Any-Time and Program-Iteration by Infinitary Conjunction.Norihiro Kamide - 2013 - Journal of Applied Non-Classical Logics 23 (3):284 - 298.
    Two new infinitary modal logics are simply obtained from a Gentzen-type sequent calculus for infinitary logic by adding a next-time operator, and a program operator, respectively. It is shown that an any-time operator and a program-iteration operator can respectively be expressed using infinitary conjunction in these logics. The cut-elimination and completeness theorems for these logics are proved using some theorems for embedding these logics into (classical) infinitary logic.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  48.  1
    Classical Linear Logics with Mix Separation Principle.Norihiro Kamide - 2003 - Mathematical Logic Quarterly 49 (2):201-209.
    Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut-elimination theorems, the completeness theorems and a characteristic property named the mix separation principle are proved for these logics.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  49. Automating and Computing Paraconsistent Reasoning: Contraction-Free, Resolution and Type Systems.Norihiro Kamide - 2010 - Reports on Mathematical Logic:3-21.
     
    Export citation  
     
    Bookmark  
  50. A Logic Of Sequences.Norihiro Kamide - 2011 - Reports on Mathematical Logic:29-57.
1 — 50 / 54