Dagstuhl Seminar 05431
Deduction and Applications
( Oct 23 – Oct 28, 2005 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/05431
Organizers
- Franz Baader (TU Dresden, DE)
- Peter Baumgartner (MPI für Informatik - Saarbrücken, DE)
- Robert Nieuwenhuis (UPC - Barcelona, ES)
- Andrei Voronkov (University of Manchester, GB)
Contact
Formal logic provides a mathematical foundation for many areas of computer science, including problem specification, program development, transformation and verification, hardware design and verification, relational databases, knowledge engineering, theorem proving, computer algebra, logic programming, and artificial intelligence.
Using computers for solving problems in these areas, therefore, requires the design and implementation of algorithms based on logical deduction. It remains one of the great challenges in informatics to make computers perform non-trivial logical reasoning, be it fully automatic, or in interaction with humans. Some progress, however, has been made in the past ten years:
- Automated theorem provers and finite model building programs solved various open mathematical problems of combinatorial nature.
- Model checking, a form of theorem proving over finite models, has become a very successful push-button method for verifying nontrivial safety properties of hardware and software.
- Automated deduction, in particular for so-called description logics, is widely assessed as a core enabling technology for the Semantic Web .
- Methods of interactive theorem proving have helped in formally verifying semantic (type) safety aspects of programming languages such as Java. The "Schwerpunktprogramm Deduktion " funded by the Deutsche Forschungsgemeinschaft together with previous Dagstuhl seminars on "Deduction" have been instrumental in obtaining these successes.
The conviction that mathematical logic is a unifying principle in computer science and that methods from different theoretical areas as well as application domains should be brought together as a means to fight fragmentation has lead to successful new conferences like FLoC and IJCAR, and to IFCoLoG, the recently established International Federation for Computational Logic.
This interdisciplinary view of logic in computer science motivated the Dagstuhl seminar. Specifically, we considered several application areas:
- Software verification
- Hardware verification
- Cryptographic protocols
- Programming languages
- Formal methods
- Semantic Web
- Large knowledge bases.
- Markus Aderhold (TU Darmstadt, DE)
- Franz Baader (TU Dresden, DE) [dblp]
- Matthias Baaz (TU Wien, AT) [dblp]
- Clark W. Barrett (New York University, US) [dblp]
- Peter Baumgartner (MPI für Informatik - Saarbrücken, DE) [dblp]
- Bernhard Beckert (Universität Koblenz-Landau, DE) [dblp]
- Christoph Benzmüller (Universität des Saarlandes, DE) [dblp]
- Alan Bundy (University of Edinburgh, GB)
- Dominique Cansell (LORIA - Nancy, FR)
- Alessandro Cimatti (Centro Ricerche FIAT - Trento, IT) [dblp]
- Koen Claessen (Chalmers UT - Göteborg, SE) [dblp]
- Hubert Comon-Lundh (ENS - Cachan, FR)
- Hans de Nivelle (MPI für Informatik - Saarbrücken, DE) [dblp]
- Bernd Fischer (NASA / RIACS - Moffett Field, US) [dblp]
- Ulrich Furbach (Universität Koblenz-Landau, DE) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Reiner Hähnle (Chalmers UT - Göteborg, SE) [dblp]
- Thomas Hillenbrand (MPI für Informatik - Saarbrücken, DE)
- Ian Horrocks (University of Manchester, GB) [dblp]
- Dieter Hutter (DFKI - Saarbrücken, DE)
- Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
- Yevgeny Kazakov (MPI für Informatik - Saarbrücken, DE) [dblp]
- Claude Kirchner (LORIA & INRIA - Nancy, FR) [dblp]
- Boris Konev (University of Liverpool, GB)
- Konstantin Korovin (University of Manchester, GB) [dblp]
- Viktor Kuncak (MIT - Cambridge, US) [dblp]
- Shuvendu K. Lahiri (Microsoft Research - Redmond, US) [dblp]
- Tal Lev-Ami (Tel Aviv University, IL)
- Carsten Lutz (TU Dresden, DE) [dblp]
- Christopher Lynch (Clarkson University - Potsdam, US) [dblp]
- Ilkka Niemelä (Helsinki University of Technology, FI)
- Robert Nieuwenhuis (UPC - Barcelona, ES) [dblp]
- Albert Oliveras (Polytechnic University of Catalonia, ES) [dblp]
- Brigitte Pientka (McGill University - Montreal, CA) [dblp]
- Ruzica Piskac (MPI für Informatik - Saarbrücken, DE) [dblp]
- Enric Rodríguez-Carbonell (UPC - Barcelona, ES) [dblp]
- Albert Rubio (UPC - Barcelona, ES) [dblp]
- Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
- Uli Sattler (University of Manchester, GB) [dblp]
- Gerhard Schellhorn (Universität Augsburg, DE) [dblp]
- Andreas Schlosser (TU Darmstadt, DE)
- Renate Schmidt (University of Manchester, GB) [dblp]
- Manfred Schmidt-Schauss (Universität Frankfurt, DE) [dblp]
- Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Stephan Schulz (TU München, DE) [dblp]
- Johann M. Schumann (NASA / RIACS - Moffett Field, US)
- Jörg Siekmann (DFKI - Saarbrücken, DE)
- John Slaney (Australian National University - Canberra, AU) [dblp]
- Viorica Sofronie-Stokkermans (MPI für Informatik - Saarbrücken, DE) [dblp]
- Gernot Stenz (TU München, DE)
- Aaron Stump (Washington University - St. Louis, US) [dblp]
- Geoff Sutcliffe (University of Miami, US) [dblp]
- Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
- Ashish Tiwari (SRI - Menlo Park, US) [dblp]
- Margus Veanes (Microsoft Research - Redmond, US) [dblp]
- Andrei Voronkov (University of Manchester, GB) [dblp]
- Arild Waaler (University of Oslo, NO) [dblp]
- Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
- Christoph Walther (TU Darmstadt, DE)
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Frank Wolter (University of Liverpool, GB) [dblp]
Related Seminars
- Dagstuhl Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
- Dagstuhl Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
- Dagstuhl Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
- Dagstuhl Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
- Dagstuhl Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
- Dagstuhl Seminar 03171: Deduction and Infinite-state Model Checking (2003-04-21 - 2003-04-25) (Details)
- Dagstuhl Seminar 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (Details)
- Dagstuhl Seminar 09411: Interaction versus Automation: The two Faces of Deduction (2009-10-04 - 2009-10-09) (Details)
- Dagstuhl Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
- Dagstuhl Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
- Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
- Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (Details)
- Dagstuhl Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
- Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
- Dagstuhl Seminar 26091: Revisiting the Foundations of Deduction in a New World (2026-02-22 - 2026-02-27) (Details)
