| CADE-19 in Miami28 July - 2 August 2003In the sunshine ... On the beach |
|
|
| CADE-19 in Miami28 July - 2 August 2003In the sunshine ... On the beach |
|
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 |
| | |