CADE-19 in Miami

28 July - 2 August 2003

In the sunshine ... On the beach

Workshop Paper Schedules


Schedule for:


W1: First QPQ Workshop on Deductive Software Components


Session 1: Monday 28th, 09:00-10:00
09:00-9:20 Invited Talk: The QPQ Deductive Software Repository
Mark Stickel
09:20-9:40 Peopleware in Practice
Tiziana Margaria
09:40-10:00 The QSL Platform at LORIA
Mohamed El Habib, Claude Kirchner, Helene Kirchner, Jean-Yves Marion, Stephan Merz

Session 2: Monday 28th, 10:30-11:30
10:30-10:50 The Calculemus Research Training Network
Chris Benzmueller
10:50-11:10 Metalogical Frameworks and QPQ
Carsten Schuermann
11:10-11:30 Discussion

Session 3: Monday 28th, 11:30-12:30
11:30-11:50 Resurrecting Analytica
Edmund Clarke, Michael Kohlhase, Joel Ouaknine, Klaus Sutner
11:50-12:10 The Interface is the Message
Sam Owre, Harald Ruess, Natarajan Shankar
12:10-12:30 Discussion

W2: Pragmatics of Decision Procedures in Automated Reasoning


Session 1: Tuesday 29th, 09:00-10:00
09:00-10:00 Invited Talk: Specialized Reasoning in SNARK
Mark Stickel

Session 2: Tuesday 29th, 10:30-12:30
10:30-11:00 Various Commonly Occurring Decidable Extensions of Multi-level Syllogistic
D. Cantone, A. Formisano, E. G. Omodeo, J. T. Schwartz
11:00-11:30 Rogue Decision Procedures
A. Stump, A. Deivanayagam, S. Kathol, D. Lingelbach, and D. Schobel
11:30-12:00 A Proof-Producing Booelan Search Engine
C. Barrett, S. Berezin, and D. Dill
12:00-12:30 Abstraction Based Theorem Proving: An example from the theory of Reals
A. Tiwari

Session 3: Tuesday 29th, 14:30-15:30
14:30-15:00 Simplifying OBDDs in Decidable Theories
A. Armando
15:00-15:30 Verifying Industrial Hybrid Systems with MathSAT
G. Audemard, M. Bozzano, A. Cimatti, and R. Sebastiani

Session 4: Tuesday 29th, 16:00-18:00
16:00-18:00 SMT-LIB Panel

W3: Challenges and Novel Applications for Automated Reasoning


Session 1: Monday 28th, 14:00-15:30
14:00-14:45 Invited Talk: The Grand Challenge of Theorem Discovery
Geoff Sutcliffe, Yi Gao, Simon Colton
14:45-15:00 A Universal Automated Information System for Science and Technology
Peter Andrews
15:00-15:15 Are there True Grand Challenges in Mechanized Mathematics?
Jacques Calmet
15:15-15:30 Concept Formation
Christoph Walther

Session 2: Monday 28th, 16:00-18:00
16:00-16:45 Panel Discussion
Toby Walsh (Moderator), Simon Colton, Stephan Schulz, Volker Sorge, Cesare Tinelli
16:45-17:10 Computer Modelling the Human Immune System
Raul Monroy
17:10-17:35 KRHyper Inside: Model Based Deduction in Applications
Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, Thomas Kleemann, Christoph Wernhard
17:35-18:00 Knowledge Representation and Scalable Abstract Reasoning for Sentient Computing using First-Order Logic
Eleftheria Katsiri, Alan Mycroft

W4: Model Computation - Principles, Algorithms, Applications


Session 1: Tuesday 29th, 09:00-10:00
09:00-10:00 Invited Talk: Model Generation Theorem Proving: Trends and Applications
Ulrich Furbach

Session 2: Tuesday 29th, 10:30-12:30
10:30-11:00 System Description: KRHyper
Christoph Wernhard
11:00-11:30 Knowledge Compilation: Decomposable Negation Normal Form versus Linkless Formulas
Neil Murray
11:30-12:00 Finite Model Building: Improvements and Comparisons
Tanel Tammet
12:00-12:30 New Techniques that Improve MACE-style Finite Model Finding
Koen Claessen, Niklas Sörensson

Session 3: Tuesday 29th, 14:00-15:30
14:00-15:00 Invited Talk: Answer Set Programming - From Model Computation to Problem Solving
Illka Niemela
15:00-15:30 Optimising Minimal Herbrand Model Generation Procedures
Lilia Georgieva

Session 4: Tuesday 29th, 16:00-18:00
16:00-16:30 Using Models to Guide a Human-Oriented Proof Search
Seungyeob Choi, Manfred Kerber
16:30-17:00 Compact Models for Multi-modal Logics
Jens Happe
17:00-17:30 Preferred Models for Ordered Resolution
Christopher Lynch