Invited Speakers

We characterize the recursively enumerable first-order Gödel logics with Delta with respect to validity and non-satisfiability. The finitely valued and four infinitely valued Gödel logics with Delta are recursively enumerable, non-satisfiability is recursively enumerable iff validity is recursively enumerable. This is in contrast to first-order Gödel logics without Delta, where validity is recursively enumerable for finitely valued and two infinitely valued Gödel logics, non-satisfiability is recursively enumerable iff validity is recursively enumerable or 0 is isolated in the truth value set.

Joint work with Norbert Preining.

De Vries duality establishes a duality between the category of compact Hausdorff spaces and complete compingent algebras e.g., Boolean algebras with a special binary relation. These algebras are also called de Vries algebras. In this talk, I will discuss logical aspects of this duality. In particular, I will define a logical system via Gabbay-like non-standard rules and prove algebraic completeness for this logic for de Vries algebras and topological completeness for compact Hausdorff spaces. I will also make comparison of this work with existing literature.

This is joint work with G. Bezhanishvili, T. Santoli, S. Sourabh, and Y. Venema.

I will show a proof system, called KV, which is a multiplicative linear logic with a self-dual non-commutative connective ‘seq’ and a self-dual modality ‘star’ providing contraction over seq. Given this characteristics, KV could form the core of a proof system for a Kleene algebra. KV can also be seen as an extension of BV with the star modality.
My interest in KV stems from its design principles. Usually, we give a computational interpretation to the normalisation procedures of existing proof systems. Contrary to this tradition, my starting point has been a certain computational behaviour, and KV arises as a way to comply with that behaviour. More specifically, the design constraints of KV consist in respecting the separation of three compression/composition mechanisms: 1) sharing/contraction, 2) reuse/cut, 3) modularity/substitution. These three mechanisms are subject to three independent normalisation procedures, respectively: 1) decomposition, 2) splitting, 3) ‘Formalism B’ normalisation.

This work helps clarifying the three mentioned techniques, which are still under development, although decomposition and splitting have been used for almost fifteen years. Nonetheless, both decomposition and splitting receive a substantial simplification in KV, and especially so compared to recent related work. One remarkable phenomenon is that under the natural and logic-independent constraints that I imposed, system KV seems to be canonical, in the sense that there is no room to manoeuvre in the design of the rules.

That quantifiers have different properties in different logics is illustrated by the Skolemization method. This method, which removes strong quantifiers from formulas, is sound and complete in classical logic but in many other logics it is not. For example, in intuitionistic logic and numerous other intermediate logics it is sound, but not complete.
The usefulness of the Skolemization method is the connection it provides between derivability in a predicate logic and its propositional fragment. Thus for logics for which the method is not complete, there still remains the question whether there is an alternative method that provides such a useful connection.
Several years ago, Matthias Baaz and I showed that in the presence of an existence predicate a method, called eskolemization, can be developed, that is sound and complete in intermediate logics, at least when only existential quantifiers are considered. For the full language such a method has not been found and may not even exist. This talk is about the intermediate logics for which eskolemization, when considered for the full language, is sound and complete.

Joint work with Matthias Baaz.

The range of ‘logics for social behaviour’ (by which I mean those logics aimed at capturing aspects such as agency and information flow) is rapidly expanding, and their theory is being intensively investigated, especially w.r.t. their semantic aspects. However, these logics typically lack a comparable proof-theoretic development. More often than not, the hurdles preventing their standard proof-theoretic development are due to the very features which make them capture essential aspects of the real world, such as their not being closed under uniform substitution, or the presence of certain extralinguistic labels and devices encoding key interactions between logical connectives.
In this talk I will focus on multi-type display-type calculi, a methodology introduced in [3, 2] to provide DEL and PDL with analytic calculi, and pursued also in [1].
Multi-type languages allow the upgrade of actions, agents, coalitions, etc. from parameters in the generation of formulas, to terms. Like formulas, they thus become first-class citizens of the framework, endowed with their corresponding structural connectives and rules. In this richer environment, many features which were insurmountable hurdles to the standard treatment can be understood as symptoms of the original languages of these logics lacking the necessary expressivity to encode certain key interactions within the language. The success of the multi-type methodology in defining analytic calculi for logics as proof-theoretically impervious as DEL lies in its providing a mathematical environment in which the expressivity problems can be clearly identified.
I will argue that multi-type display-type calculi can provide a platform for a uniform proof theoretic account of the logics for social behaviour.

References
[1] M. Bílková, V. Dignum, G. Greco, A. Palmigiano, and A. Tzimoulis. Logic of resources and capabilities. In preparation.
[2] S. Frittella, G. Greco, A. Kurz, and A. Palmigiano. Multi-type display calculus for propositional dynamic logic. Journal of Logic and Computation, Special Issue on Substructural Logic and Information Dynamics, 2014.
[3] S. Frittella, G. Greco, A. Kurz, A. Palmigiano, and V. Sikimić. Multi-type display calculus for dynamic epistemic logic. Journal of Logic and Computation, Special Issue on Substructural Logic and Information Dynamics, 2014.

Consider a propositional formula which is equivalent to its negation. Existence of such a formula is inconsistent with substructural logics above FLc, whereas consistent with those below Łukasiewicz logic. More generally, we can think of substructural logics extended with arbitrary mutual fixpoints. In this talk, we review some elementary properties of those logics and explain why it is important to study them.

Formally specifying privacy goals is not trivial. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. A subtle question is how we can be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal. To address this problem, we introduce a novel and declarative way to specify privacy goals, called “alpha-beta privacy”, and relate it to static equivalence. This new approach is based on specifying two formulae alpha and beta in first-order logic with Herbrand universes, where alpha reflects the intentionally released information and beta includes the actual cryptographic (“technical”) messages the intruder can see.
Then alpha-beta privacy means that the intruder cannot derive any “non-technical” statement from beta that he cannot derive from alpha already. We describe by a variety of examples how this notion can be used in practice. Even though alpha-beta privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools, and obtain partial tool support for alpha-beta privacy.

Joint work with Sebastian Mödersheim and Thomas Groß.