37 found
Sort by:
  1. Norihiro Kamide (2013). A Hierarchy of Weak Double Negations. 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)  
     
    My bibliography  
     
    Export citation  
  2. Norihiro Kamide (2013). Representing Any-Time and Program-Iteration by Infinitary Conjunction. 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.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Norihiro Kamide (2013). Temporal Gödel-Gentzen and Girard Translations. Mathematical Logic Quarterly 59 (1):66-83.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Norihiro Kamide (2012). Bounded Linear-Time Temporal Logic: A Proof-Theoretic Investigation. Annals of Pure and Applied Logic 163 (4):439-466.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Norihiro Kamide (2012). Combining Intuitionistic Logic with Paraconsistent Operators. Logique Et Analyse 217:57-71.
     
    My bibliography  
     
    Export citation  
  6. Norihiro Kamide (2011). Cut-Elimination and Completeness in Dynamic Topological and Linear-Time Temporal Logics. Logique Et Analyse 215:379-394.
     
    My bibliography  
     
    Export citation  
  7. Norihiro Kamide (2011). Notes on Craig Interpolation for LJ with Strong Negation. Mathematical Logic Quarterly 57 (4):395-399.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Norihiro Kamide & Heinrich Wansing (2011). Completeness and Cut-Elimination Theorems for Trilattice Logics. Annals of Pure and Applied Logic 162 (10):816-835.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Heinrich Wansing & Norihiro Kamide (2011). Synchronized Linear-Time Temporal Logic. 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 (7 more)  
     
    My bibliography  
     
    Export citation  
  10. Norihiro Kamide (2010). An Embedding-Based Completeness Proof for Nelson's Paraconsistent Logic. Bulletin of the Section of Logic 39 (3/4):205-214.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  11. Norihiro Kamide (2010). Dynamic Non-Commutative Logic. Journal of Logic, Language and Information 19 (1):33-51.
    A first-order dynamic non-commutative logic (DN), 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 (tree-based) reasoning.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  12. Norihiro Kamide (2010). Strong Normalization of Program-Indexed Lambda Calculus. Bulletin of the Section of Logic 39 (1/2):65-78.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  13. Norihiro Kamide & Heinrich Wansing (2010). Symmetric and Dual Paraconsistent Logics. 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)  
     
    My bibliography  
     
    Export citation  
  14. Norihiro Kamide (2009). Proof Systems Combining Classical and Paraconsistent Negations. 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)  
     
    My bibliography  
     
    Export citation  
  15. Norihiro Kamide (2009). Temporal Non-Commutative Logic: Expressing Time, Resource, Order and Hierarchy. 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)  
     
    My bibliography  
     
    Export citation  
  16. Norihiro Kamide & Heinrich Wansing (2009). Sequent Calculi for Some Trilattice Logics. 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)  
     
    My bibliography  
     
    Export citation  
  17. Motohiko Mouri & Norihiro Kamide (2008). Strong Normalizability of Typed Lambda-Calculi for Substructural Logics. 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)  
     
    My bibliography  
     
    Export citation  
  18. Norihiro Kamide (2007). Extended Full Computation-Tree Logics for Paraconsistent Model Checking. 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)  
     
    My bibliography  
     
    Export citation  
  19. Norihiro Kamide (2007). Synthesized Substructural Logics. 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.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  20. Norihiro Kamide (2007). Towards a Theory of Resource: An Approach Based on Soft Exponentials. Journal of Applied Non-Classical Logics 17 (1):63-89.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. Norihiro Kamide (2007). Temporalizing Linear Logic. Bulletin of the Section of Logic 36 (3/4):173-182.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  22. Norihiro Kamide & Motohiko Mouri (2007). Natural Deduction Systems for Some Non-Commutative Logics. 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)  
     
    My bibliography  
     
    Export citation  
  23. Norihiro Kamide (2006). Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation. 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)  
     
    My bibliography  
     
    Export citation  
  24. Norihiro Kamide (2005). A Cut-Free System for 16-Valued Reasoning. Bulletin of the Section of Logic 34 (4):213-226.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  25. Norihiro Kamide (2005). Cut-Free Single-Succedent Systems Revisited. Bulletin of the Section of Logic 34 (3):165-175.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  26. Norihiro Kamide (2005). Gentzen-Type Methods for Bilattice Negation. 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)  
     
    My bibliography  
     
    Export citation  
  27. Norihiro Kamide (2005). Natural Deduction Systems for Nelson's Paraconsistent Logic and its Neighbors. Journal of Applied Non-Classical Logics 15 (4):405-435.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  28. Norihiro Kamide (2005). On a Logic of Involutive Quantales. Mathematical Logic Quarterly 51 (6):579-585.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  29. Norihiro Kamide (2004). A Relationship Between Rauszer's HB Logic and Nelson's Logic'. Bulletin of the Section of Logic 33 (4):237-249.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  30. Norihiro Kamide (2004). Quantized Linear Logic, Involutive Quantales and Strong Negation. Studia Logica 77 (3):355 - 384.
    A new logic, quantized intuitionistic linear logic (QILL), is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's (commutative) 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)  
     
    My bibliography  
     
    Export citation  
  31. Norihiro Kamide (2003). A Note on Dual-Intuitionistic Logic. Mathematical Logic Quarterly 49 (5):519.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  32. Norihiro Kamide (2003). Classical Linear Logics with Mix Separation Principle. Mathematical Logic Quarterly 49 (2):201-209.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Norihiro Kamide (2003). Normal Modal Substructural Logics with Strong Negation. 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)  
     
    My bibliography  
     
    Export citation  
  34. Norihiro Kamide (2002). Kripke Semantics for Modal Substructural Logics. 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)  
     
    My bibliography  
     
    Export citation  
  35. Norihiro Kamide (2002). Substructural Logics with Mingle. 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)  
     
    My bibliography  
     
    Export citation  
  36. Norihiro Kamide (2001). A Note on Decision Problems for Implicational Sequent Calculi. Bulletin of the Section of Logic 30 (3):129-138.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  37. Ryo Kashima & Norihiro Kamide (1999). Substructural Implicational Logics Including the Relevant Logic E. 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)  
     
    My bibliography  
     
    Export citation