63 found
Order:
  1.  26
    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   7 citations  
  2.  20
    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)  
    Translate
     
     
    Export citation  
     
    Bookmark   3 citations  
  3.  16
    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   6 citations  
  4.  24
    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   4 citations  
  5.  62
    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  
  6.  15
    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   4 citations  
  7.  12
    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   2 citations  
  8.  8
    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)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  9.  12
    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   1 citation  
  10.  42
    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  
  11.  15
    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  
  12.  23
    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  
  13.  9
    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)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  14.  12
    Combining Linear-Time Temporal Logic with Constructiveness and Paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
  15.  9
    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  
  16.  24
    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  
     
    Export citation  
     
    Bookmark   8 citations  
  17.  85
    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   7 citations  
  18.  38
    A Relationship Between Rauszer's HB Logic and Nelson's Logic'.Norihiro Kamide - 2004 - Bulletin of the Section of Logic 33 (4):237-249.
  19.  11
    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   9 citations  
  20.  29
    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  
  21.  36
    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  
  22.  14
    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  
  23.  41
    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   5 citations  
  24.  33
    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  
  25.  28
    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   3 citations  
  26.  17
    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  
  27.  16
    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  
  28.  13
    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  
  29.  45
    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   3 citations  
  30.  36
    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  
  31. 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  
  32. 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  
  33.  11
    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  
  34.  7
    Falsification-Aware Semantics and Sequent Calculi for Classical Logic.Norihiro Kamide - 2022 - 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)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  35. 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  
  36.  33
    An Embedding-Based Completeness Proof for Nelson's Paraconsistent Logic.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (3/4):205-214.
  37.  27
    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  
  38.  45
    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 (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  39.  11
    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  
  40. A Logic Of Sequences.Norihiro Kamide - 2011 - Reports on Mathematical Logic:29-57.
  41. Bunched Sequential Information.Norihiro Kamide - 2016 - Journal of Applied Logic 15:150-170.
  42. Cut-Elimination and Completeness in Dynamic Topological and Linear-Time Temporal Logics.Norihiro Kamide - 2011 - Logique Et Analyse 54 (215):379-394.
  43. Extended Full Computation-Tree Logics For Paraconsistent Model Checking.Norihiro Kamide - 2006 - Logic and Logical Philosophy 15:251-267.
    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, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.
     
    Export citation  
     
    Bookmark  
  44. Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-Time Temporal Logic.Norihiro Kamide - 2012 - Reports on Mathematical Logic:29-61.
     
    Export citation  
     
    Bookmark  
  45. Combining Intuitionistic Logic with Paraconsistent Operators.Norihiro Kamide - 2012 - Logique Et Analyse 217:57-71.
  46.  27
    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 (7 more)  
     
    Export citation  
     
    Bookmark  
  47.  24
    Temporalizing Linear Logic.Norihiro Kamide - 2007 - Bulletin of the Section of Logic 36 (3/4):173-182.
    Direct download  
     
    Export citation  
     
    Bookmark  
  48.  5
    Correction to: Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - 2020 - Journal of Philosophical Logic 49 (6):1213-1213.
    The original version of this article unfortunately contains several errors introduced by the typesetter during the publishing process. It has been corrected.
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  49.  21
    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  
  50.  1
    Embedding Friendly First-Order Paradefinite and Connexive Logics.Norihiro Kamide - forthcoming - Journal of Philosophical Logic:1-48.
    First-order intuitionistic and classical Nelson–Wansing and Arieli–Avron–Zamansky logics, which are regarded as paradefinite and connexive logics, are investigated based on Gentzen-style sequent calculi. The cut-elimination and completeness theorems for these logics are proved uniformly via theorems for embedding these logics into first-order intuitionistic and classical logics. The modified Craig interpolation theorems for these logics are also proved via the same embedding theorems. Furthermore, a theorem for embedding first-order classical Arieli–Avron–Zamansky logic into first-order intuitionistic Arieli–Avron–Zamansky logic is proved using a modified (...)
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
1 — 50 / 63