We consider the fragment of propositional multi-modal logic that consists of implications whose premise and conclusion are strictly positive (SP) modal formulas constructed from propositional variables using conjunction and unary diamond operators. SP-logics can be interpreted over bounded meet-semilattices with normal monotone operators (SLOs, for short), and over first-order structures (aka Kripke frames). The former interpretation provides natural calculi for SP-logics, while reasoning over the latter can be supported by modern provers and description logic reasoners, and is often tractable. An SP-logic is called (Kripke) complete if it has the same consequences in each of these semantics. This talk reports on our first steps in developing completeness theory for SP-logics, which turns out to be quite different from classical completeness theory for modal logics. We also consider some related problems, in particular, axiomatisability and computational complexity.

Constructible sheaves play an important role in several areas of mathematics, most notably in the theory of D-modules. It was proved by Kashiwara and Schapira that the category of constructible sheaves is closed under the standard six operations of Grothendieck. This result can be viewed as a far reaching generalization of the Tarski-Seidenberg principle in real algebraic geometry. In this talk I will describe some quantitative/effectivity results related to the Kashiwara-Schapira theorem – mirroring similar results for ordinary semi-algebraic sets which are now well known. For this purpose, I will introduce a measure of complexity of constructible sheaves, and bound the complexity of some of the standard sheaf operations in terms of this measure of complexity. I will also discuss quantitative bounds on the dimensions of cohomology groups of constructible sheaves in terms of their complexity, again extending similar results on bounding the the ordinary Betti numbers of semi-algebraic sets.

We provide a lower complexity bound for the satisfiability problem of a multi-agent justification logic, establishing that there are certain NEXP-complete multi-agent justification logics with interactions. We then use a simple modification of the corresponding reduction to prove that satisfiability for all multi-agent justification logics in a general class we consider is $Sigma_2^p$-hard — given certain reasonable conditions. Our methods improve on these required conditions for the same lower bound for the single-agent justification logics, proven by Buss and Kuznets in 2009, thus answering one of their open questions.

Link to paper on arXiv:
http://arxiv.org/abs/1503.00362

The three topics in the title have been inextricably linked since the famous 1912 paper of Max Dehn. In recent years the asymptotic-generic point of view of geometric group theory has given rise to new areas of computability and computational complexity. I will discuss how this arose and then focus on one recent development in computability theory, namely, coarse computability and the coarse computability bound.

Separation Logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Alternatively, there are a lot of activities to develop verification methods with decision procedures for fragments of practical use.

Actually, there exist many versions or fragments of Separation Logic that can be viewed as fragments of Second-Order Logic, as well as variants of Modal or Temporal Logics in which models can be updated dynamically (as in Public Announcement Logic).

In this talk, after introducing first principles on Separation Logic, issues related to decidability, computational complexity and expressive power are discussed. We provide several tight relationships with Second-Order Logic, Interval Temporal Logic or Data Logics, depending on the variants of the logic and on the syntactic resources available.

Results presented during the talk span from standard ones about Separation Logic to more recent ones, some of them obtained in collaboration with Dr. Morgan Deters (NYU, CIMS).

The complexity of Modal Logic has been extensively studied. Ladner has established most of what are now considered classical results on the matter, determining that most of the usual modal logics are PSPACE-complete. Furthermore, as Chagrov and Rybakov showed, some of these logics remain PSPACE-complete even for their variable-free fragments. We present parameters of modal formulas whose effect on the complexity of modal logic has been studied – like modal depth – and we identify sources of complexity for modal satisfiability.

A big part of this talk is joint work with Michael Lampis and Valia Mitsou.

We introduce a family of multi-agent justification logics with interactions between the agents’ justifications, by extending and generalizing the two-agent versions of LP introduced by Yavorskaya in 2008. Known concepts and tools from the single-agent justification setting are adjusted for this multiple agent case. We present tableau rules and some preliminary complexity results: in several important cases, the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while for others it is PSPACE or EXP-hard.

This week we will present the general tableau rules for the family. We look more closely at particular examples and complexity bounds and we identify common sources of jumps in their complexity.

We introduce a family of multi-agent justification logics with interactions between the agents’ justifications, by extending and generalizing the two-agent versions of LP introduced by Yavorskaya in 2008. Known concepts and tools from the single-agent justification setting are adjusted for this multiple agent case. We present tableau rules and some preliminary complexity results: in several important cases, the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while for others it is PSPACE or EXP-hard.