This is the homepage of the BRICS Logic in Computer Science Semantics seminar. Its activities roughly correspond to those areas covered by the LICS conference. The seminars will continue the activities of the earlier BRICS-CLICS Frokost and the BRICS Logic Seminars.The seminars are the meeting point for the logic group at BRICS and for people interested in category theory and semantics.
Below you will find the speakers of our recent seminars as well as annoucements of forthcoming seminars. For titles and abstracts of previous seminars, please look at the web-pages for the BRICS-CLICS Frokost and the BRICS Logic Seminars.
The seminar maintains a mailing list called brics-lics-seminar. Mails send to brics-lics-seminar@brics.dk are directly redirected to all the members of this list. If you want to be on this list (or off), contact one of the persons in charge of the seminar (see bottom of the page).
If you would like to contribute with a talk, please contact one of the persons in charge of the seminar.
Abstract:
The talk is supposed to present a brief survey of main results in the
logic of proofs.
Logic of proofs formulated in the format `t is a proof of F' was
found by S.Artemov in 1995. Here t is the exact term representing the
proof constructed with the help of three elementary recursive
operations on proofs. The system LP of logic of proofs is shown to be
complete with the intended semantics. It suffices to realize the
entire S4 and therefore intuitionistic logic which allows to give the
exact provability interpretation for both of them.
Except the results mentioned above we touch upon the following topics
1. The joint logic of proofs and provability (T. Yavorskaya).
2. Logic of single-conclusion proofs (V. Krupski).
3. Quantifier versions of logic of proofs (S.Artemov, T.Yavorskaya,
R.Yavorsky).
4. Explicit modal logics (S.Artemov, E.Kazakov, D.Shapiro)
Abstract:
In this talk I will investigate the decidability of history-preserving
bisimilarity (HPB) and hereditary history-preserving bisimilarity (HHPB)
for basic parallel processes (BPP). I will show that both notions are
decidable for this class of infinite systems, and present tableau-based
decision procedures.
The result for HPB has already been established by Kiehn and Hennessy
via the decidability of causal bisimilarity, a notion that is
equivalent to HPB. However, the decision procedure presented in this talk
provides an independent and direct proof. The decidability of HHPB for BPP
is a new result, and is especially interesting, when considering that the
decidability of HHPB is still open for finite-state systems.
Abstract:
The talk is based on joint reasearch with Zhaohui Luo (Durham). First
of all, the approach to subtyping as an abbreviational mechanism will
be outlined. It is essentially represented by so called "coercive
definition rule" which allows to write equalities like f(x)=f(c(x))
where f:A-->B, x:A_0 (A_0 is a subtype of A) and c:A_0-->A is
the corresponding coercion. The role of conservativity problem
in this approach will be explained. Our results corresponding to
difficult case of dependent types systems with user-defined part
(such as coercions between inductive types) will be presented.
New notion of dependent coercion (proposed recently by Z. Luo)
and related notion of covering (proposed by S. Soloviev) will
be introduced and their possible applications discussed (for example,
definition of fractal type, applications to geometry).
Abstract:
A class of structures obeys a 0-1 law if every first-order sentence
has an asymptotic probability of 0 or 1 within the
class. Techniques used to prove 0-1 laws are closely related to
average-case analyses of algorithms. For example, Abiteboul,
Compton and Vianu showed that the 0-1 law for random relational
structures (which includes random graphs with constant edge
probabilities) can be used to give an average-case analysis of
certain database query optimizations. However, the random graph
model is not a very realistic model for databases, so it is
useful to examine other structures. A map, or embedding of
a graph into a surface of fixed genus, may be a better model
of certain kinds of geometric databases. Bender, Compton,
and Richmond showed that the class of random maps in surface
of fixed genus obeys a 0-1 law. We will analyze the complexity
of the problem of deciding whether a given sentence has a probability
of 1, and argue that it is unlikely that query optimization algorithms
will give significant improvements on random maps.
Abstract:
We report on recent results on the computational and
mathematical strength of extensions
of the binary Koenig's lemma WKL. In particular, we consider a uniform
version UWKL of WKL which
asserts the existence of a functional selecting an infinite path of a
given infinite binary tree.
It turns out that the computational strength (in terms of provably total
programs) of UWKL crucially
depends on the amount of extensionality which is available in the
underlying base system .
This phenomenon shows that the addition of the extensionality axiom to a
weakly extensional system
(based on a Spector-style rule of extensionality) can increase the
computational strength of the system enormously.
Finally we will argue that it is the combination of extensionality with
classical logic (Markov's principle)
which constitutes one of the most serious stumbling blocks in
developing a computational interpretation
of non-constructive proofs for higher order objects.
Abstract:
Drawing inspiration from the theory of finite automata on infinite
objects, I give a new (as far as I know) refinement of the so-far
known characterization of the power of the game quantifier in
effective descriptive set theory.
I'll probably not talk about the proof, which is not hard, but just
explain what the above means!
Abstract:
In models for concurrency like e.g. labelled
synchronisation trees, any infinite path is implicitly assumed to be
admissible. In particular, recursion is always to be interpreted as
"possibly infinite recursion". This is not always appropriate, e.g. if
one wants to describe fairness, some infinite runs should be ruled out
as inadmissible. I will describe a presheaf model (making use
of a simple topology) that supports explicit observation of infinite
paths. I'll sketch how Milners calculus SCCS can be modelled in this
category, using maximal fixed points as denotation for (possibly
infinite) recursion and minimal fixed points for finite recursion
(e.g. finite delay).
Abstract:
The talk will focus on a special kind of tiling problems.
These tiling problems are related to complexity gaps in
propositional proof complexity for a certain class of
algebraic proof systems.