Search

It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theorems are shown for some fragments and extensions of LTL. These theorems are simply proved based on an embedding-based proof method with Gentzen-type sequent calculi. Maksimova separation theorems (Maksimova principle of variable separation) are also shown for these LTL variants. [ABSTRACT FROM AUTHOR]

In this paper, we prove some embedding theorems for LTL (linear-time temporal logic) and its variants: viz. some generalisations, extensions and fragments of LTL. Using these embedding theorems, we give uniform proofs of the completeness, cut-elimination and/or decidability theorems for LTL and its variants. The proposed embedding theorems clarify the relationships between some LTL-variations (for example, LTL, a dynamic topological logic, a fixpoint logic, a spatial logic, Prior's logic, Davies' logic and an NP-complete LTL) and some traditional logics (for example, classical logic, intuitionistic logic and infinitary logic). [ABSTRACT FROM AUTHOR]

Strong normalization theorems are uniformly proved for typed lambda calculi for a family of temporal substructural logics including some temporal non-commutative logics. [ABSTRACT FROM AUTHOR]

Linear-time temporal logics (LTLs) are known to be useful for verifying concurrent systems, and a simple natural deduction framework for LTLs has been required to obtain a good computational interpretation. In this paper, a typed λ-calculus λB[l] with a Curry-Howard correspondence is introduced for an in- tuitionistic bounded linear-time temporal logic B[l], of which the time domain is bounded by a fixed positive integer l. The strong normalization theorem for λB[l] is proved as a main result. The base logic B[l] is defined as a Gentzen-type sequent calculus, and despite the restriction on the time domain, B[l] can derive almost all the typical temporal axioms of LTLs. The proposed framework allows us to obtain a uniform and simple proof-theoretical treatment of both natural deduction and sequent calculus, i.e., the equivalence between them, the cut-elimination theorem, the decidability theorem, the Curry-Howard correspondence and the strong normalization theorem can be obtained uniformly. [ABSTRACT FROM AUTHOR]

In this article, some paraconsistent and temporal description logics are studied based on an embedding-based proof method. A new paraconsistent description logic, PALC, is obtained from the description logic ALC by adding a paraconsistent negation. Two temporal description logics, XALC and BALCl, are introduced by combining and modifying ALC and Prior’s tomorrow tense logic. XALC has the next-time operator, and BALCl has some restricted versions of the next-time, any-time and some-time operators, in which the time domain is bounded by a positive integer l. Some theorems for embedding PALC, XALC and BALCl into ALC are proved in a uniform way, and PALC, XALC and BALCl are shown to be decidable. Three tableau calculi for PALC, XALC and BALCl are introduced, and the completeness theorems for these calculi are proved. [ABSTRACT FROM AUTHOR]

It is known that linear-time temporal logic (LTL) 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. [ABSTRACT FROM PUBLISHER]

We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN3 introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and 2006, Journal of Logic, Language and Information, 15, 403–424). In a first step, a logic I16 is presented as a Gentzen-type sequent calculus for an intuitionistic version of Odintsov’s Hilbert-style axiom system LT (Kamide and Wansing, 2009, Review of Symbolic Logic, 2, 374–395; Odintsov, 2009, Studia Logica, 91, 407–428). The cut-elimination theorem for I16 is proved using an embedding of I16 into Gentzen’s LJ. The completeness theorem with respect to a Kripke-style semantics is also proved for I16. The framework of I16 is regarded as plausible and natural for the following reasons: (i) the properties of constructible falsity and paraconsistency with respect to some negation connectives hold for I16, and (ii) sequent calculi for Belnap and Dunn’s four-valued logic (Anderson et al., 1992, Entailment: The Logic of Relevance and Necessity; Belnap, 1977, A useful four-valued logic, In Modern uses of Multiple Valued Logic, pp. 5–37; Dunn, 1976, Philosophical Studies, 29, 149–168) and for Nelson’s constructive four-valued logic (Almukdad and Nelson, 1984, Journal of Symbolic Logic, 49, 231–233) are included as natural subsystems of I16. In a second step, a logic IT16 is introduced as a tableau calculus. The tableau system IT16 is an intuitionistic counterpart of Odintsov’s axiom system for truth entailment ⊨t in SIXTEEN3 and of the sequent calculus for ⊨t presented in Wansing (2010, Journal of Philosophical Logic, to appear). The tableau calculus is also shown to be sound and complete with respect to a Kripke-style semantics. A tableau calculus for falsity entailment can be obtained by suitably modifying the notion of provability. [ABSTRACT FROM PUBLISHER]

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic. [ABSTRACT FROM AUTHOR]

Cut-elimination property, relevance principle, interpolation property and a new property named communication principle are proved for a number of modal intuitionistic linear logics with communication-merge rules. A concurrent-computational interpretation for these logics is obtained based on a process algebra with communication-merge. [ABSTRACT FROM PUBLISHER]

A new logic, spatio-temporal soft linear logic, which has soft linear exponential, linear exponential and spatio-temporal operators, is introduced as a sequent calculus. A Petri net interpretation and an informational interpretation for this logic are given by using simple complete semantics. By using this logic and these interpretations, various kinds of spatio-temporal and resource-sensitive reasoning can be expressed. [ABSTRACT FROM PUBLISHER]

We introduce intuitionistic and classical substructural logics with structural rules mingle and connective strong negation, and investigate the cut‐elimination property and the relevance principle for these logics. The relevance principle does not hold for substructural logics with mingle and usual negation, but holds for those with mingle and strong negation. [ABSTRACT FROM PUBLISHER]

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. [ABSTRACT FROM PUBLISHER]

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 logic. [ABSTRACT FROM AUTHOR]

The original version of this article unfortunately contains several errors introduced by the typesetter during the publishing process. It has been corrected. [ABSTRACT FROM AUTHOR]

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 is also shown to be decidable and embeddable into S4. [ABSTRACT FROM AUTHOR]