As a first exploration of base-extension semantics for substructural logics, we extend Sandqvist's sound and complete base-extnsion semantics for IPL to intuitionistic multiplicative linear logic (IMLL), a minimal fragment of intuitionistic linear logic (ILL) consisting of the multiplicative conjunction and implication. The two key technical choices are: first, we define a supporting relation relative to some atomic multisets viewed as resource; second, semantics of the connectives are defined in terms of their corresponding elimination rules. These enable to establish the soundness and completeness following Sandqvist's treatment for IPL. It opens the door to base-extension semantics to substructural logics, including logic of bunched implication (BI), linear logic, relevant logic. 

We develop a diagrammatic calculus for SAT. We provide a poset-enriched axiomatisation theory, in terms of string diagrams, that is sound and complete for monotone relations between finite Boolean algebras. This can be seen as a reminiscent of the diagrammatic calculus for nondeterministic finite automata. We apply this diagrammatic calculus to the Boolean satisfiability problem as well as definite propositional logic programming. In particular, the logic programming part is a continuation of the previous exploration of reasoning (variants of) logic programming diagrammatically under functorial semantics. 

This is a first step towards a uniform diagrammatic treatment of (propositional) logic programming and its quantitative variants (probabilistic and weighted). The observation is that the structural similarity of the clauses and the semantic distinction can be nicely separately under the functorial semantics framework, where the infenrential structure of the clauses belong to the syntactic categories, and the meaning of the programs is determined by the chosen semantic category. Such a uniform picture provides mathematical context for comparison with other computational models. For instance, we illustrate how the tranformation between (Boolean-valued) Bayesian networks and (acyclic) probabilistic logic programs can be characterised precisely as operations on the syntax (of string diagrams). 

This is a journal version of the conference paper "Coalgebraic perspective on probabilistic logic programming". In particular, we extend the work to a large class of weighted logic programs.  

We proved the Henessey-Milner property of probabilistic propositional dynamic logic (PPDL), namely it characterises trace equivalence. In addition, we presented an extension of PPDL that characterises the strongder notion of probabilistic bisimulation. We also provided a short discussion of a categorical unification of PDL and PPDL. 

We presented a coalgebraic semantics for probabilistic logic programming, both propositional and first-order case. 

We presented an alternative presentation of the "knowing value" logic. The observation is that, since the values for variables do not appaer explicitly in the modal formulas, we may replace such values in the Kripke models with a ternary relation representing the mismatch of the value of certain variable x in two accessible states from the current state, thus leading to the lack of knowledge of the value of x. As a result, we can present the "knowing value" logic as a normal modal logic, and apply canonical strategy for. e.g. soundness and completeness proofs. 

A categorical generalisation of the probabilistic and relational models for the logic dependence and independence bunched implication (DIBI) is given. The "input-preserving kernels" are intuitively characterised as the image of certain "input-preserving string diagrams" under suitable functors. This entail a large class of DIBI models, e.g. continuous probabilistic DIBI models.