|
July 11, 2011
And Logic Begat Computer Science: When Giants Roamed the Earth
During the past fifty years there has been extensive, continuous,
and growing interaction between logic and computer science.
In fact, logic has been called "the calculus of computer
science". The argument is that logic plays a fundamental
role in computer science, similar to that played by calculus
in the physical sciences and traditional engineering disciplines.
Indeed, logic plays an important role in areas of computer
science as disparate as architecture (logic gates), software
engineering (specification and verification), programming
languages (semantics, logic programming), databases (relational
algebra and SQL), artificial intelligence (automated theorem
proving), algorithms (complexity and expressiveness), and
theory of computation (general notions of computability).
This non-technical talk will provide an overview of the
unusual effectiveness of logic in computer science by surveying
the history of logic in computer science, going back all
the way to Aristotle and Euclid, and showing how logic actually
gave rise to computer science.
July 12, 2011
From Philosophical to Industrial Logics
One of the surprising developments in the area of program
verification is how several ideas introduced by logicians
in the first part of the 20th century ended up yielding
at the start of the 21st century industry-standard property-specification
languages called PSL and SVA. This development was enabled
by the equally unlikely transformation of the mathematical
machinery of automata on infinite words, introduced in the
early 1960s for second-order arithmetics, into effective
algorithms for industrial model-checking tools. This talk
attempts to trace the tangled threads of this development.
July 13, 2011
Logic, Automata, Games, and Algorithms
The automata-theoretic approach to decision procedures,
introduced by Buechi, Elgot, Rabin and Trakhtenbrot in the
1950s and 1960s, is one of the most fundamental approaches
to decision procedures. Recently, this approach has found
industrial applications in formal verification of hardware
and software systems. The path from logic to practical algorithms
goes not only through automata, but also through games,
whose algorithmic aspects were studies by Chandra, Kozen,
and Stockmeyer in the late 1970s. In this overview talk
we describe the path from logic to algorithms via automata
and games.
Moshe Vardi is a Professor of Computer Science at Rice University,
USA. He is the Karen Ostrum George Professor in Computational
Engineering and Director of the Computer and Information Technology
Institute. His interests focus on applications of logic to
computer science, including database theory, finite-model
theory, knowledge in multi-agent systems, computer-aided verification
and reasoning, and teaching logic across the curriculum. He
is a renowned expert in model checking, constraint satisfaction
and database theory, common knowledge (logic), and theoretical
computer science.
Moshe Y. Vardi is the author of over 300 technical papers
as well as the editor of several collections. He has authored
the books Reasoning About Knowledge with Ronald Fagin,
Joseph Y. Halpern, and Yoram Moses, and Finite Model Theory
and Its Applications with Erich Grädel, Phokion G.
Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Yde Venema,
and Scott Weinstein. He is also the editor-in-chief of Communications
of the ACM.
Vardi is the recipient of three IBM Outstanding Innovation
Awards, a co-winner of the 2000 Gödel Prize, a co-winner
of the 2005 ACM Paris Kanellakis Theory and Practice Award,
and a co-winner of the LICS 2006 Test-of-Time Award. He holds
honorary doctorates from Saarland University, Germany, and
the University of Orleans, France. Dr Vardi is an editor of
several international journals and the president of the International
Federation of Computational Logicians. He is a Guggenheim
Fellow, as well as a Fellow of the Association of Computing
Machinery, the American Association for the Advancement of
Science, and the American Association for Artificial Intelligence.
He was designated Highly Cited Researcher by the Institute
for Scientific Information, and was elected as a member of
the US National Academy of Engineering, the European Academy
of Sciences, and the Academia Europea. He has also co-chaired
the ACM Task Force on Job Migration.
|
