
Logical Models of Reasoning and Computation
Steklov Mathematical Institute
February 13, 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 nonclassical 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 finitelyvalued 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 nonmonotonicity 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 nonclassical logics.
 Nachum Dershowitz
Canonical Inference

An abstract prooftheoretic framework, inspired by rewriting methods, is
proposed. Normalform proof objects are minimal in some wellfounded
proof ordering. The approach applies in the equational, Hornclause,
and deductionmodulo 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 Mooresentences (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 brickandmortar (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&Mtocloud 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_{1} and h_{2}
so that A holds for h_{1} and
B holds for h_{2}.
In my talk I will address the following issues.
 General separation models, and concrete heaplike models
of practical interest.
 Inplace reasoning, the frame property, the weakest preconditions,
inductive definitions (linked lists, trees),
within separation logic used as an extension of Hoare logic.
 As for the assertion language of separation logic, even purely
propositional separation logic turns out to be undecidable.
What is more, whatever concrete heaplike 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.
 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 nontrivial 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
`pointsto' predicate, and an inductive predicate for describing
linkedlist segments. Standard entailment turns out to be decidable
in polytime, while abduction ranges from NPcomplete to polytime
for different subproblems. The following parametrized complexity
is of great practical and theoretical importance — that is,
the NPcompleteness 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
GerbrandyGroeneveld'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_{1} (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 contextfree languages without the
empty word, and L_{1}grammars generate precisely all contextfree
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 prooftheoretically weak
systems of Feferman's explicit mathematics and theories of truth. We start off from
pure firstorder 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 prooftheoretic strength of the soobtained 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 truththeoretic 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 nonuniform
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 nonnegative 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 wellknown method to eliminate one type of quantifier
from formulas and (cutfree) 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 speedup. 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 firstorder case it was established that the most natural
axiomatizability questions for the firstorder logic of proofs
have negative answers (S. Artemov, T. Yavorskaya, 2001).
The questions of provability reading for firstorder
S4 and the firstorder intuitionistic logic HPC remained open until 2011.
In my talk I am going present the firstorder logic of proofs FOLP and
its exact interpretation in formal systems (e.g., in Peano Arithmetic).
FOLP is capable of realizing firstorder S4 and, therefore, HPC.
This provides a semantics of explicit proofs for firstorder S4 and HPC
compliant with BrouwerHeytingKolmogorov requirements. Joint work with
S. Artemov.
 Michael Zakharyaschev
On ontologybased 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 firstorder 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 worstcase size and the
"realworld" practical size of such rewritings and discuss some emerging
problems.
 Anna Zamansky
Modular Construction of Cutfree 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 cutfree calculi for thousands of paraconsistent logics known
as Logics of Formal (In)consistency (LFIs). The method relies on
nondeterministic semantics for these logics, and produces in a modular way
uniform Gentzentype 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 multimodal 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).

