Variants of derivation modes for which catalytic P systems with one catalyst are computationally complete

Catalytic P systems are among the first variants of membrane systems ever considered in this area. This variant of systems also features some prominent computational complexity questions, and in particular the problem of using only one catalyst: is one catalyst enough to allow for generating all recursively enumerable sets of multisets? Several additional ingredients have been shown to be sufficient for obtaining even computational completeness with only one catalyst. Last year we could show that the derivation mode $$max_{objects}$$ m a x objects , where we only take those multisets of rules which affect the maximal number of objects in the underlying configuration one catalyst is sufficient for obtaining computational completeness without any other ingredients. In this paper we follow this way of research and show that one catalyst is also sufficient for obtaining computational completeness when using specific variants of derivation modes based on non-extendable multisets of rules: we only take those non-extendable multisets whose application yields the maximal number of generated objects or else those non-extendable multisets whose application yields the maximal difference in the number of objects between the newly generated configuration and the current configuration. A similar computational completeness result can even be obtained when omitting the condition of non-extendability of the applied multisets when taking the maximal difference of objects or the maximal number of generated objects. Moreover, we reconsider simple P system with energy control—both symbol and rule energy-controlled P systems equipped with these new variants of derivation modes yield computational completeness.

Somebody Knows

Several different notions of group knowledge have been extensively studied in the epistemic and doxastic logic literature, including common knowledge, general knowledge (everybody-knows) and distributed knowledge. In this paper we study a natural notion of group knowledge between general and distributed knowledge: somebody-knows. While something is general knowledge if and only if it is known by everyone, this notion holds if and only if it is known by someone. This is stronger than distributed knowledge, which is the knowledge that follows from the total knowledge in the group. We introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike the other mentioned group knowledge modalities, somebody-knows is not a normal modality; in particular it lacks the conjunctive closure property. We provide an equivalent neighbourhood semantics for the language with a single somebody-knows modality, together with a completeness result: the somebody-knows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom. We also show that the satisfiability problem for this logic is PSPACE-complete. The neighbourhood semantics and the completeness and complexity results also carry over to logics for so-called local reasoning (Fagin et al. 1995) with bounded ``frames of mind'', correcting an existing completeness result in the literature (Allen 2005).

Axiomatizing Hybrid XPath with Data

In this paper we introduce sound and strongly complete axiomatizations for XPath with data constraints extended with hybrid operators. First, we present HXPath=, a multi-modal version of XPath with data, extended with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath=, and we prove it is strongly complete with respect to the class of abstract data models, i.e., data models in which data values are abstracted as equivalence relations. We prove a general completeness result similar to the one presented in, e.g., [BtC06], that ensures that certain extensions of the axiomatic system we introduce are also complete. The axiomatic systems that can be obtained in this way cover a large family of hybrid XPath languages over different classes of frames, for which we present concrete examples. In addition, we investigate axiomatizations over the class of tree models, structures widely used in practice. We show that a strongly complete, finitary, first-order axiomatization of hybrid XPath over trees does not exist, and we propose two alternatives to deal with this issue. We finally introduce filtrations to investigate the status of decidability of the satisfiability problem for these languages.

Negation and Implication in Quasi-Nelson Logic

Quasi-Nelson logic is a recently-introduced generalization of Nelson’s constructive logic with strong negation to a non-involutive setting. In the present paper we axiomatize the negation-implication fragment of quasi-Nelson logic (QNI-logic), which constitutes in a sense the algebraizable core of quasi-Nelson logic. We introduce a finite Hilbert-style calculus for QNI-logic, showing completeness and algebraizability with respect to the variety of QNI-algebras. Members of the latter class, also introduced and investigated in a recent paper, are precisely the negation-implication subreducts of quasi-Nelson algebras. Relying on our completeness result, we also show how the negation-implication fragments of intuitionistic logic and Nelson’s constructive logic may both be obtained as schematic extensions of QNI-logic.

From Hilbert proofs to consecutions and back

Restall set forth a "consecution" calculus in his An Introduction to Substructural Logics. This is a natural deduction type sequent calculus where the structural rules play an important role. This paper looks at different ways of extending Restall's calculus. It is shown that Restall's weak soundness and completeness result with regards to a Hilbert calculus can be extended to a strong one so as to encompass what Restall calls proofs from assumptions. It is also shown how to extend the calculus so as to validate the metainferential rule of reasoning by cases, as well as certain theory-dependent rules.

Parameterised complexity of model checking and satisfiability in propositional dependence logic

Dependence Logic was introduced by Jouko Väänänen in 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of PDL is NP-complete (Ebbing and Lohmann, SOFSEM 2012). The subject of this research is to identify a list of parameterisations (formula-size, formula-depth, treewidth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that the number of disjunctions or the arity of dependence atoms (dep-arity) as a parameter both yield a paraNP-completeness result. Then, we consider the satisfiability problem (SAT) which classically is known to be NP-complete as well (Lohmann and Vollmer, Studia Logica 2013). There we are presenting a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is FPT. Finally, we introduce a variant of the satisfiability problem, asking for a team of a given size, and show for this problem an almost complete picture.

Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance

We prove the SOS strategy for first-order resolution to be refutationally complete on a clause set N and set-of-support S if and only if there exists a clause in S that occurs in a resolution refutation from $$N\cup S$$ N ∪ S . This strictly generalizes and sharpens the original completeness result requiring N to be satisfiable. The generalized SOS completeness result supports automated reasoning on a new notion of relevance aiming at capturing the support of a clause in the refutation of a clause set. A clause C is relevant for refuting a clause set N if C occurs in every refutation of N. The clause C is semi-relevant, if it occurs in some refutation, i.e., if there exists an SOS refutation with set-of-support $$S = \{C\}$$ S = { C } from $$N\setminus \{C\}$$ N \ { C } . A clause that does not occur in any refutation from N is irrelevant, i.e., it is not semi-relevant. Our new notion of relevance separates clauses in a proof that are ultimately needed from clauses that may be replaced by different clauses. In this way it provides insights towards proof explanation in refutations beyond existing notions such as that of an unsatisfiable core.

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming

A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed the invariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is by far the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition—thereby synthesizing invariant barrier certificates—can be encoded as solving an optimization problem subject to bilinear matrix inequalities (BMIs). We further propose a synthesis algorithm based on difference-of-convex programming, which approaches a local optimum of the BMI problem via solving a series of convex optimization problems. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmark examples demonstrate the effectiveness and efficiency of our approach.

Internal coalgebras in cocomplete categories: Generalizing the Eilenberg–Watts theorem

The category of internal coalgebras in a cocomplete category [Formula: see text] with respect to a variety [Formula: see text] is equivalent to the category of left adjoint functors from [Formula: see text] to [Formula: see text]. This can be seen best when considering such coalgebras as finite coproduct preserving functors from [Formula: see text], the dual of the Lawvere theory of [Formula: see text], into [Formula: see text]: coalgebras are restrictions of left adjoints and any such left adjoint is the left Kan extension of a coalgebra along the embedding of [Formula: see text] into [Formula: see text]. Since [Formula: see text]-coalgebras in the variety [Formula: see text] for rings [Formula: see text] and [Formula: see text] are nothing but left [Formula: see text]-, right [Formula: see text]-bimodules, the equivalence above generalizes the Eilenberg–Watts theorem and all its previous generalizations. By generalizing and strengthening Bergman’s completeness result for categories of internal coalgebras in varieties, we also prove that the category of coalgebras in a locally presentable category [Formula: see text] is locally presentable and comonadic over [Formula: see text] and, hence, complete in particular. We show, moreover, that Freyd’s canonical constructions of internal coalgebras in a variety define left adjoint functors. Special instances of the respective right adjoints appear in various algebraic contexts and, in the case where [Formula: see text] is a commutative variety, are coreflectors from the category [Formula: see text] into [Formula: see text].

A Preference-Based Approach to Defeasible Deontic Inference

In this paper we present an approach to defeasible deontic inference. Given a set of rules R expressing conditional obligations and a formula A giving contingent information, the goal is to determine the most desirable outcome with respect to this information. Semantically, the rules R induce a partial preorder on the set of models, giving the relative desirability of each model. Then the set of minimal A models characterises the best that can be attained given that A holds. A syntactic approach is also given, in terms of maximal subsets of material counterparts of rules in R, and that yields a formula that expresses the best outcome possible given that A holds. These approaches are shown to coincide, providing an analogue to a soundness and completeness result. Complexity is not unreasonable, being at the second level of the polynomial hierarchy when the underlying logic is propositional logic. The approach yields desirable and intuitive results, including for the various “paradoxes” of deontic reasoning. The approach also highlights an interesting difference in how specificity is dealt with in nonmonotonic and deontic reasoning.