In this paper we give relational semantics and an accompanying relational proof system for a variety of intuitionistic substructural logics, including linear logic with exponentials. Starting with the semantics for FL as discussed in [13], we developed, in [11], a relational semantics and a relational proof system for full Lambek calculus. Here, we take this as a base and extend the results to deal with the various structural rules of exchange, contraction, weakening and expansion, and also to deal with an (...) involution operator and with the operators ! and ? of linear logic. To accomplish this, for each extension X of FL we develop a Kripke-style semantics, RelKripkeX semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with distinguished elements, ternary relations and a list of conditions on the relations. For each extension X, RelKripkeX semantics is accompanied by a Kripke-style valuation system analogous to that in [13]. Soundness and completeness theorems with respect to FLX hold for RelKripkeX-models. Then, in the spirit of the work of Orlowska [16], [17], and Buszkowski & Orlowska [4], we develop relational logic RFLX for each extension X. The adjective relational is used to emphasize the fact that RFLX has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ→α in FLX is provable if, a translation, t<εvu, has a cut-complete proof tree which is fundamental. This result is constructive: that is, if a cut-complete proof tree for tεvu is not fundamental, we can use the failed proof search to build a relational countermodel for t and from this, build a RelKripkeX countermodel for γ1[sdot ]…[sdot ]γn⊃α. (shrink)

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)

We introduce Kripke models for propositional substructural logics with strong negation, and show the completeness theorems for these logics using an extended Ishihara's canonical model construction method. The framework presented can deal with a broad range of substructural logics with strong negation, including a modified version of Nelson's logic N$^-$, Wansing's logic COSPL, and extended versions of Visser's basic propositional logic, positive relevant logics, Corsi's logics and M\'endez's logics.

The completeness between linear logic and Petri nets has been shown for several versions of linear logic. For example, Engberg and Winskel considered the [sqcup ]-free fragment of propositional intuitionistic linear logic without exponential ¡, and showed soundness and completeness of the logic for a Petri net model. One of difficulties in proving completeness for full propositional intuitionalistic linear logic lies in distributivity of [sqcap ] over [sqcup ], that is not valid in linear logic. The quantales constructed by Engberg (...) and Winskel are distributive lattices, i.e., distributivity is always valid. In this paper, we first construct non-distributive quantales from Petri nets by using a closure operation, and prove completeness of full linear logic without exponential for them. Next we extend the construction of the quantales to those with exponential ¡, and prove completeness of linear logic with exponential for the quantales. We also give an impression on the meaning of the logic on the proposed Petri net model, comparing with that by Engberg and Winskel. (shrink)