Logic List Mailing Archive

7.3.2003; Utrecht: Theoriedag 2003 van de NVTI (Fortnow, Stevenhagen, Vardi, de Rijke)

Theoriedag 2003 van de NVTI
  (Nederlandse Vereniging voor Theoretische Informatica)

PLEASE NOTE : the announcement is in dutch, only the abstracts are in
english; for more (english) information please email Jan Willem Klop
<J.W.Klop@cwi.nl>. ALSO PLEASE NOTE : If you want to take part in the
organised lunch (euro 14) you can either call or email Susanne van Dam:
020-592 4189 / <susanne@cwi.nl> before February 28.

Vrijdag 7 maart 2003
Vergadercentrum Hoog Brabant
Radboudkwartier 23
Hoog Catharijne
Utrecht

Het is ons een genoegen u uit te nodigen tot het bijwonen van de
Theoriedag 2003 van de NVTI, de Nederlandse Vereniging voor Theoretische
Informatica, die zich ten doel stelt de theoretische informatica te
bevorderen en haar beoefening en toepassingen aan te moedigen. De
Theoriedag 2003 zal gehouden worden op vrijdag 7 maart aanstaande, in
Vergadercentrum Hoog Brabant te Utrecht, gelegen in winkelcenrum Hoog
Catharijne, op enkele minuten loopafstand van CS Utrecht, en is een
voortzetting van de reeks jaarlijkse bijeenkomsten van de NVTI die acht
jaar geleden met de oprichtingsbijeenkomst begon.

Evenals vorige jaren hebben wij een aantal prominente sprekers uit binnen-
en buitenland bereid gevonden deze dag gestalte te geven met voordrachten
over recente en belangrijke stromingen in de theoretische informatica.
Naast een wetenschappelijke inhoud heeft de dag ook een informatief
gedeelte, in de vorm van een algemene vergadering waarin de meest
relevante informatie over de NVTI gegeven zal worden, alsmede presentaties
van de onderzoekscholen.

Programma (samenvattingen volgen beneden)
---------

9.30-10.00: Ontvangst met koffie
10.00-10.10: Opening
10.10-11.00: Lezing Prof.dr. L. Fortnow (Nec Laboratories America)
             Titel: Church, Kolmogorov and von Neumann:
                    Their Legacy Lives in Complexity
11.00-11.30: Koffie
11.30-12.20: Prof.dr. P. Stevenhagen (UL)
             Titel: Primes is in P
12.20-12.50: Presentatie Onderzoeksscholen
             (OZL, IPA, SIKS)
12.50-14.10: Lunch (Zie beneden voor registratie)
14.10-15.00: Lezing Prof.dr. M. Vardi (Rice University, USA)
             Titel: The Design of A Formal Property-Specification
                    Language
15.00-15.20: Thee
15.20-16.10: Lezing Dr. M. de Rijke (UvA)
             Titel: Intelligent Information Access
16.10-16.40: Algemene ledenvergadering NVTI

ABSTRACTS

Prof.dr. L. Fortnow (Nec Laboratories, USA)
Church, Kolmogorov and von Neumann: Their Legacy Lives in Complexity

In the year 1903, several of the greatest early computer scientists
entered our world. In this talk we look at the work of three of these
giants: Alonzo Church, Andrey Kolmogorov and John von Neumann honoring the
100th anniversary of their births. We will focus on how their research has
and continues to play a major role in the development of computational
complexity and our understanding of what we can compute.

Alonzo Church developed the lambda-calculus, a computation model
equivalent to the Turing machine. He co-developed independently with Alan
Turing what we now call the Church-Turing thesis that states that every
computable is computable by a Turing machine (or the lambda-calculus).

John von Neumann's work in quantum mechanics, game theory, automata theory
and his development of early computers have played major roles in the
development of algorithms and complexity.

We will spend most of the seminar discussing the influence of Andrey
Kolmogorov, whose work on algorithmic randomness has had a more direct
impact on computational complexity and certainly my own research. We will
give an overview of Kolmogorov complexity and several examples of
computational restricted versions of this measure have helped us better
understand the nature of efficient computation.



Prof.dr. P. Stevenhagen (UL)
Primes is in P

In August 2002, the Indian computer scientists Agrawal, Kayal and Saxena
proved that primality of an integer can be tested by means of a
deterministic algorithm that runs in polynomial time. For several decades,
this had been an outstanding problem. We discuss the importance of the
result in theory and practice, and give an impression of the mathematics
that goes into it.


Prof.dr. M. Vardi (Rice University, USA)
The Design of A Formal Property-Specification Language

In recent years, the need for formal specification languages is growing
rapidly as the functional validation environment in semiconductor design
is changing to include more and more validation engines based on formal
verification technologies.  In particular, the usage of Formal Equivalence
Verification and Formal Property Verification is growing, new symbolic
simulation engines are introduced and hybrid environments of scalar and
symbolic simulators are developed. To facilitate the use of these
new-generation validation engines - properties, checkers and reference
models need to be developed in a formal language.

In this talk we describe the design of the ForSpec Temporal Logic (FTL),
the new temporal logic of ForSpec, Intel's new formal
property-specification language, which is today part of Synopsis OpenVera
hardware verification language (www.open-vera.com). The key features of
FTL are: it is a linear temporal logic, based on Pnueli's LTL, it enables
the user to define temporal connectives over time windows, it enables the
user to define regular events, which are regular sequences of Boolean
events, and then relate such events via special connectives, and it
contains constructs that enable the user to model multiple clock and reset
signals, which is useful in the verification of globally asynchronous and
locally synchronous hardware designs.

The focus of the talk is on design rationale, rather than a detailed
language description.


Dr. M. de Rijke (UvA)
Intelligent Information Access

Search is one of the core topics in theoretical computer science, and
online search has become a day-to-day activity for many of us. Finding
keywords in a text file is easy. Using keyword search, current retrieval
systems allow users to find documents that are relevant to their
information needs, but most leave it to the user to extract the useful
information from those documents.  This leaves the (often unwilling) user
with a relatively large amount of text to consume.  People have questions
and they need answers, not documents.  There is a need for tools that
reduce the amount of text one might have to read to obtain the desired
information.

In this talk I review ongoing research initiatives (such as novelty
detection, question answering, and XML retrieval) aimed at moving beyond
traditional document retrieval, and I will try to identify theoretical
issues that arise from these initiatives.