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 (...) calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory. (shrink)

A spatial modal logic is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut-elimination theorem for a modified subsystem of SML are also presented.