This paper investigates (modal) extensions of Heyting-Brouwer logic, i.e., the logic which results when the dual of implication (alias coimplication) is added to the language of intuitionistic logic. We first develop matrix as well as Kripke style semantics for those logics. Then, by extending the Gö;del-embedding of intuitionistic logic into S4, it is shown that all (modal) extensions of Heyting-Brouwer logic can be embedded into tense logics (with additional modal operators). An extension of the Blok-Esakia-Theorem is proved for this embedding.

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 (...) extension or generalization of Hodas and Miller's dual-context calculus appearing in a linear logic programming language. Second, we present a concurrent process calculus based on the logic. This calculus is an extension of Okada's process calculus. Third, we introduce a Kripke type semantics for a fragment of the logic, and show the completeness theorems with respect to the semantics. Finally, we mention a logic programming language based on the triple-context calculus. (shrink)

The sequent system LDJ is formulated using the same connectives as Gentzen's intuitionistic sequent system LJ, but is dual in the following sense: (i) whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii) whereas LJ has the same sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain a (...) more precise mapping, both LJ and LDJ are extended by adding a "pseudo-difference" operator which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems and , and a simply consistent but -inconsistent Set Theory with Unrestricted Comprehension Schema based on LDJ is sketched. (shrink)

It is shown that the constructive four-valued logic N4 can be faithfully embedded into the modal logic S4. This embedding is used to obtain complete, cut-free display sequent calculi for N4 and C4, the modal logic of consistency over N4. C4 is a natural monotonic base system for semantics-based non-monotonic reasoning.

ABSTRACT In the paper we present a survey of some approaches to the semantics of many-valued propositional systems. These approaches are inspired on one hand by classical problems in the investigations of logical aspects of epistemic activity: knowledge and truth, contradictions, beliefs, reliability of data, etc. On the other hand they reflect contemporary concerns of researchers in Artificial Intelligence (and Cognitive Science in general) with inferences drawn from imperfect information, even from total ignorance. We treat the mathematical apparatus that has (...) emerged recently: algebraic structures related to the new logical systems in the same way Boolean algebras correspond to classical logic. (shrink)

It is shown that the constructive four-valued logic N4 can be faithfully embedded into the modal logic S4. This embedding is used to obtain complete, cut-free display sequent calculi for N4 and C4, the modal logic of consistency over N4. C4 is a natural monotonic base system for semantics-based non-monotonic reasoning.