Theoriedag 2003 van de NVTI De activiteiten van de NVTI worden mede mogelijk gemaakt door de ondersteuning (financieel en anderszins) van de volgende instellingen: NWO/EW, CWI, de Onderzoeksscholen SIKS, IPA, OZSL, Elsevier Science B.V. Vrijdag 7 maart 2003 Vergadercentrum Hoog Brabant Radboudkwartier 23 Hoog Catharijne Utrecht 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 en 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 Samenvattingen van de lezingen ------------------------------ 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 andcontinues 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.