Logical Models of Reasoning and Computation
Steklov Mathematical Institute
February 1-3, 2012
- 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
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
- 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
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
h1 and h2
so that A holds for h1 and
B holds for h2.
In my talk I will address the following issues.
- General separation models, and concrete heap-like models
of practical interest.
- In-place 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 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.
- 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
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.)
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: L1 (adding the unit
constant) and LR (adding a unary connective that corresponds to taking the
language of the inverse strings). We prove that L(\;p)-grammars and
LR-grammars generate precisely all context-free languages without the
empty word, and L1-grammars generate precisely all context-free
- 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.
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.)
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.
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
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.
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
- 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
- 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
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).