Logical Models of Reasoning and Computation
Steklov Mathematical Institute
February 1-3, 2012

Preliminary Program

Sergei Adian
On a method of proving exact bounds on derivational complexity in length preserving Thue systems

Matthias Baaz
Epsilon theorems and non-classical logics

We show, that the presence of critical formulas allows for the derivation of arbitrary quantifier shifts in almost all nonclassical logics. This result is used to derive that the only superintuitionistic logics admitting the first epsilon theorem are the finitely-valued Gödel logics. They also admit the second epsilon theorem. (Joint work with Richard Zach.)

Andreas Blass and Yuri Gurevich
What is the intrinsic logic of infons?

This investigation is motivated by Distributed Knowledge Authorization Language (DKAL). Infons are pieces of information communicated between principals as declarative sentences. We analyze the intrinsic logic of infons and argue that, in the case when a principal’s knowledge can only increase, it is a conservative extension of intuitionistic logic. In addition, we argue that, although some non-monotonicity is inescapable in DKAL, it can be confined to infons expressing the current time, like now is February 1, 2012.

Nikolaj Bjorner

TBA

Agata Ciabattoni
Nonclassical Proofs: theory, applications, and tools

I will describe a recently funded research project aiming to systematize proof theory for non-classical logics.

Nachum Dershowitz
Canonical Inference

An abstract proof-theoretic framework, inspired by rewriting methods, is proposed. Normal-form proof objects are minimal in some well-founded proof ordering. The approach applies in the equational, Horn-clause, and deduction-modulo cases, among others, as they incorporate formal notions of simplification and redundancy.

Hans van Ditmarsch
Dynamic Epistemic Logic

I will introduce various logics for change of knowledge and belief, that have become known under the name 'Dynamic Epistemic Logic'. The basic logic of public announcements, proposed by Jan Plaza in 1989, serves to formalize logic puzzles such as 'muddy children', and 'consecutive numbers'. But much more is possible in this setting, and there are generalizations to private actions, combining information change with factual change, and so on. I will point out some relations with AGM belief revision, with Moore-sentences (p is true and you don't know that p) and with knowability (is everything knowable? no!). The topic remains much in the limelight, latest developments are about protocols, and quantifying over information change, and protocol synthesis/planning. I will give a sprinkling of such topics as well.

Yuri Gurevich
Distributed Knowledge Authorization Language (DKAL). Managing Policies and Trust

With the advent of cloud computing, the necessity arises to manage policies and trust automatically and efficiently. In a brick-and-mortar (B&M) setting, clerks learn unwritten policies from trustworthy peers. And if they don't know a policy, they know whom to ask. In the B&M-to-cloud transition, the clerks disappear. Policies have to be explicit and managed automatically. The more challenging problem yet is how to handle the interaction of the policies of distrustful principals, especially in federated scenarios where there is no central authority. The Distributed Knowledge Authorization Language (DKAL) was created to deal with such problems. We give a quick introduction to DKAL.

Max Kanovich
How and Why Separation Logic is an exact fit for Resource Reasoning about Programs

Separation logic, invented by John C. Reynolds and Peter O'Hearn, has proven to be an effective formalism for the analysis of programs that manipulate memory (in the form of pointers, heaps, stacks, etc.).

In addition to the standard propositional connectives, the most important feature of separation logic is its separating conjunction (A*B) which holds for a portion of memory, a heap h, iff h can be split into separate h₁ and h₂ so that A holds for h₁ and B holds for h₂.

In my talk I will address the following issues.

1. General separation models, and concrete heap-like models of practical interest.
2. In-place reasoning, the frame property, the weakest preconditions, inductive definitions (linked lists, trees), within separation logic used as an extension of Hoare logic.
3. As for the assertion language of separation logic, even purely propositional separation logic turns out to be undecidable. What is more, whatever concrete heap-like model H we take, it is undecidable whether a purely propositional formula A is valid in this model H. A number of propositional systems which approximate separation logic are undecidable as well. In particular, these include both Boolean BI and Classical BI. Oddly enough, Intuitionistic BI is still decidable.
4. Abduction, the problem of discovering hypotheses that support a conclusion, has mainly been studied in the context of philosophical logic and AI. Recently, the abduction principle — given A and B, find a non-trivial X such that A*X entails B, is one of the powerful practical tools for iterated deduction and hypothesis formation to `dig information out of bare code'. We study the complexity of abduction for a relevant fragment of separation logic over `symbolic heaps' which include a basic `points-to' predicate, and an inductive predicate for describing linked-list segments. Standard entailment turns out to be decidable in polytime, while abduction ranges from NP-complete to polytime for different sub-problems. The following parametrized complexity is of great practical and theoretical importance — that is, the NP-completeness notwithstanding, there is a polytime procedure for finding a solution to abduction but degree of the polynomial is proportional to the number of `list segment' subformulas in B.

Roman Kuznets
Realizing Public Announcements by Justifications

Modal public announcement logics study how public announcements affect changes in beliefs of the agents. What cannot be expressed in these logics, however, is the exact reasons for the updated beliefs. Justification Logic suggests a way of filling this gap by representing evidence and/or justifications for agents' beliefs in the object language. We present two alternative justification counterparts of Gerbrandy-Groeneveld's logic of public introspective announcements over the basic modal logic K. In particular, we show that erasing justifications for belief in either of the two suggested counterparts yields a valid modal statement about announcements. For the opposite direction, we establish a constructive procedure for restoring justifications within modalities, a process called realization, for one of the suggested counterparts provided the modalities occur outside of announcements. We discuss how recording more information about announcements in our system of justifications in the other suggested counterpart creates difficulties for applying the method of "realization by reduction" we have developed.
(Joint work with Samuel Bucheli and Thomas Studer, University of Bern.)

Stepan Kuznetsov
Grammars based on variants of the Lambek calculus

We consider the Lambek calculus with one division and one primitive type (L(\;p)) and two extensions of the Lambek calculus: L₁ (adding the unit constant) and L^R (adding a unary connective that corresponds to taking the language of the inverse strings). We prove that L(\;p)-grammars and L^R-grammars generate precisely all context-free languages without the empty word, and L₁-grammars generate precisely all context-free languages.

Alexei Semenov, Sergei Soprunov
The Lattice of Relational Algebras Definable in Integers with Successor

We consider relational algebras (logically closed sets of relations) that are smaller than algebra of relations definable in structure of integers with successor. A complete description of all these algebras and their lattice is given.

Thomas Strahm
Types and truth in weak applicative theories

In this talk we survey recent developments in the study of proof-theoretically weak systems of Feferman's explicit mathematics and theories of truth. We start off from pure first-order applicative theories based on a version of untyped combinatory logic and augment them by the typing and naming discipline of explicit mathematics or, alternatively, by a truth predicate in the sense of Frege structures. We discuss the proof-theoretic strength of the so-obtained formalisms and the general relationship between weak truth theories and explicit mathematics. In particular, we consider two truth theories TPR and TPT of primitive recursive and feasible strength. The latter theory is a novel abstract truth-theoretic setting which is able to interpret expressive feasible subsystems of explicit mathematics, bounded arithmetical systems, and unfoldings of feasible arithmetic.
(Joint work with Sebastian Eberhard.)

Nikolay Vereshchagin
On abstract resource semantics and computabilty logic

We show that the uniform validity is equivalent to the non-uniform validity for Blass' semantics of [A. Blass, A game semantics for linear logic, Ann. Pure Appl. Logic 56 (1992) 183–220]. We present a shorter proof (than that of [G. Japaridze, The intuitionistic fragment of computability logic at the propositional level, Ann. Pure Appl. Logic 147 (3) (2007) 187–227]) of the completeness of the positive fragment of intuitionistic logic for this semantics, computability logic semantics, and the abstract resource semantics.

Mikhail Volkov
P(l)aying for synchronization

Two topics will be presented: synchronization games and synchronization costs. In a synchronization game on a deterministic finite automaton, there are two players, Alice (Synchronizer) and Bob (Desynchronizer), whose moves alternate. Alice who pays first wants to synchronize the given automaton, while Bob aims to make her task as hard as possible. We answer a few natural questions related to such games. Speaking about synchronization costs, we consider deterministic weighted automata, that is, deterministic automata in which each transition has a certain price being a non-negative integer. The problem is whether or not we can synchronize a given automaton within a given budget. We determine the complexity of this problem.

Andrei Voronkov

TBA

Daniel Weller
Deskolemization, Equality and Logical Complexity

Skolemization is a well-known method to eliminate one type of quantifier from formulas and (cut-free) proofs. We are interested in questions about proof complexity (in the sense of logical complexity, i.e. the number of sequents in a proof): how much shorter can a proof of the Skolemization of F be when compared to proofs of F? We will show that in the presence of the equality schema, there exists an arbitrary speed-up. The result is proved using techniques from the generalization of proofs.

Tatiana Yavorskaya
First order logic of proofs

The propositional logic of proofs LP (S. Artemov, 1995) revealed an explicit provability reading of modal logic S4 and thereby provided a provability semantics for the propositional intuitionistic logic. In the first-order case it was established that the most natural axiomatizability questions for the first-order logic of proofs have negative answers (S. Artemov, T. Yavorskaya, 2001). The questions of provability reading for first-order S4 and the first-order intuitionistic logic HPC remained open until 2011. In my talk I am going present the first-order logic of proofs FOLP and its exact interpretation in formal systems (e.g., in Peano Arithmetic). FOLP is capable of realizing first-order S4 and, therefore, HPC. This provides a semantics of explicit proofs for first-order S4 and HPC compliant with Brouwer-Heyting-Kolmogorov requirements. Joint work with S. Artemov.

Michael Zakharyaschev
On ontology-based data access

In my talk, I am going to discuss recent results on the computational complexity of answering conjunctive queries to databases via ontologies. Such queries are known to be first-order rewritable over ontologies formulated in the OWL 2 QL profile of the Web Ontology Language OWL 2 and various dialects of Datalog+-. I analyse both the worst-case size and the "real-world" practical size of such rewritings and discuss some emerging problems.

Anna Zamansky
Modular Construction of Cut-free Calculi for Paraconsistent Logics

In this talk we focus on the problem of automatization of paraconsistent reasoning. We describe a general method for a systematic generation of cut-free calculi for thousands of paraconsistent logics known as Logics of Formal (In)consistency (LFIs). The method relies on non-deterministic semantics for these logics, and produces in a modular way uniform Gentzen-type rules, corresponding to a variety of schemata considered in the literature of LFIs.
(Joint work with Arnon Avron and Beata Konikowska).

Evgeny Zolin
Graded Dependent Modal Logics

This research is motivated by applications of modal logics to knowledge representation, in particular, by the research in description logics (DLs). In order to formulate the results, we need to specify three things.
First, the language we consider is the extension of the multi-modal language by the so called graded modalities, which mean that a formula holds in at least (or at most) n successors of a given world.
Secondly, the classes of Kripke frames we are interested in are determined by two kinds of constraints: (1) some accessibility relation is transitive; (2) some accessibility relation is contained in some other one. A finite collection of such constraints is called an RBox (a term used in the DL research community).
Thirdly, the reasoning problem. Typically, the main problem investigated in modal logic is that of validity, or dually, local satisfiability of formulas: whether a given formula holds in some world of some Kripke model (from a given class). On the contrary, in DLs a crucial role is played by the problem of global satisfiability: whether a given formula holds in all worlds of some Kripke model (from a given class).
We present results on (un)decidability of the global satisfiability problem of graded modal formulas in the classes of frames determined by various RBoxes. In our setting, the decidability of the problem depends only on the choice of an RBox. We also discuss some related decidability and complexity results in modal logic, show their relationship to the research in DL and, finally, list some open problems.
This is a joint work with Yevgeny Kazakov (Oxford University).