| Session 1. Invited talk | ||
| 9:00 - 10.00 | Frank Wolter | Monodic fragments of first-order temporal logics: 2000--2001 A.D.
(invited talk) |
| Coffee break | ||
| Session 2. Verification | ||
| 10.30 - 11.00 | Orna Kupferman and Moshe Vardi | On Bounded Specifications |
| 11.00 - 11.30 | Klaus Schneider | Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy |
| 11.30 - 12.00 | Volker Diekert and Paul Gastin | Local Temporal Logic is
Expressively Complete for Cograph Dependence Alphabets |
| Lunch | ||
| Session 3. Guarded Logics | ||
| 13.30 - 14.00 | Dietmar Berwanger and Erich Grädel | Games and Model Checking for Guarded Logics |
| 14.00 - 14.30 | Lilia Georgieva, Ullrich Hustadt, and Renate A. Schmidt |
Computational space efficiency and minimal model generation for guarded formulae |
| Coffee break | ||
| Session 4. Agents | ||
| 15.00 - 15.30 | Natasha Alechina and Brian Logan | Logical omniscience and the cost of deliberation |
| 15.30 - 16.00 | Sebastian Sardina | Local Conditional High-Level Robot Programs |
| 16.00 - 16.30 | Kai Engelhardt, Ron van der Meyden, and Yoram Moses |
A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents |
| Session 5. Automated Theorem Proving. | ||
| 16.45 - 17.15 | Reinhold Letz and Gernot Stenz | Proof and Model Generation with Disconnection Tableaux |
| 17.15 - 17.45 | Joseph D. Horton | Counting the Number of Equivalent Binary Resolution Proofs |
| Session 6. Invited talk | ||
| 9:00 - 10.00 | Matthias Baaz | Generalization of Proofs and Analogical Reasoning
(invited talk) |
| Coffee break | ||
| Session 7. Automated Theorem Proving | ||
| 10.30 - 11.00 | Hans de Nivelle | Splitting through New Proposition Symbols |
| 11.00 - 11.30 | Christopher Lynch and Barbara Morawska | Complexity of Linear Standard Theories |
| 11.30 - 12.00 | Matthias Baaz, Agata Ciabattoni, and Christian G. Fermueller |
Herbrand's Theorem for Prenex Godel Logic and its Consequences for Theorem Proving |
| Lunch | ||
| Session 8. Non-standard logics | ||
| 13.30 - 14.00 | Franz Baader and Ralf Kuesters | Unification in a Description Logic with Transitive Closure of Roles |
| 14.00 - 14.30 | Guy Perrier | Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions |
| Coffee break | ||
| Session 9 || 10. Types | ||
| 15.00 - 15.30 | Yong Luo and Zhaohui Luo | Coherence and transitivity in coercive subtyping |
| 15.30 - 16.00 | Carsten Schuermann | A Type-Theoretic Appropach to Induction for Higher-order Encodings |
| 16.00 - 16.30 | Jan-Georg Smaus | Analysis of Polymorphically Typed Logic Programs Using ACI-Unification |
| Session 10 || 9. Experimental papers | ||
| 15.00 - 15.30 | Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa |
Model Generation with Boolean Constraints |
| 15.30 - 16.00 | Bijan Afshordel, Thomas Hillenbrand, and Christoph Weidenbach |
First-Order Atom Definitions Extended |
| 16.00 - 16.30 | Thomas Marthedal Rasmussen | Automated Proof Support for Interval Logics |
| Session 11. Logical Foundations | ||
| 16.45 - 17.15 | Daniel Leivant | The functions provable by first order abstraction |
| 17.15 - 17.45 | Kai Brunnler and Alwen Fernato Tiu | A Local System for Classical Logic |
| Session 11A || 11B. Discussion | ||
| 10.00 - 17.00 | Discussion | LPAR |
| Session 11B || 11A. Excursion | ||
| 10.00 - 17.00 | Excursion | Beach |
| Conference dinner (19:00) |
| Session 12. Invited talk | ||
| 9:00 - 10.00 | Manuel Hermenegildo | The design of a next
generation (C)LP system
(invited talk) |
| Coffee break | ||
| Session 13. CSP and SAT | ||
| 10.30 - 11.00 | Jussi Rintanen | Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae |
| 11.00 - 11.30 | Toby Walsh | Permutation Problems and Channelling Constraints |
| 11.30 - 12.00 | Alvaro del Val | Simplifying Binary Propositional Theories into Connected Components Twice as Fast |
| Lunch | ||
| Session 14. Non-monotonic reasoning | ||
| 13.30 - 14.00 | Thomas Eiter, Michael Fink, Giuliana Sabbatini, and Hans Tompits |
Reasoning about Evolving Nonmonotonic Knowledge Bases |
| 14.00 - 14.30 | Andreas Behrend | Efficient Computation of the Well-Founded Model Using Update Propagation |
| Coffee break | ||
| Session 15 || 16. Semantics | ||
| 15.00 - 15.30 | Gianluca Amato and James Lipton | Indexed Categories and Bottom-Up Semantics of Logic Programs |
| 15.30 - 16.00 | F.J. Lopez-Fraguas and J. Sanchez-Hernandez | Functional Logic Programming with Failure: a Set-oriented View |
| 16.00 - 16.30 | Stephan Kreutzer | Operational Semantics for Fixed-Point Logics on Constraint Databases |
| Session 16 || 15. Experimental papers | ||
| 15.00 - 15.30 | Susana Munoz, Juan Jose Moreno, and Manuel Hermenegildo |
Efficient Negation Using Abstract Interpretation |
| 15.30 - 16.00 | Sylvain Boulme and Gregoire Hamon | Certifying synchrony for free |
| 16.00 - 16.30 | David McMath, Marianna Rozenfeld, and Richard Sommer |
A Computer Environment for Writing Ordinary Mathematical Proofs |
| Session 17. Termination | ||
| 16.45 - 17.15 | Alexander Serebrenik and Danny De Schreye | On termination of meta-programs |
| 17.15 - 17.45 | Cristina Borralleras and Albert Rubio | A Monotonic Higher-Order Semantic Path Ordering |
| Session 18. Knowledge-based systems | ||
| 9:00 - 9.30 | Robert Baumgartner, Sergio Flesca, and Georg Gottlob |
The Elog Web Extraction Language |
| 9:30 - 10.00 | Enrico Franconi, Antonio Lauretti Palma, Nicola Leone, Simona Perri, and Francesco Scarcello |
Census Data Repair: a challenging application of Disjunctive Logic Programming |
| Coffee break | ||
| Session 19. Analysis of Logic Programs | ||
| 10.30 - 11.00 | Roberto Bagnara, Enea Zaffanella, Roberta Gori, and Patricia M. Hill |
Boolean Functions for Finite-Tree Dependencies |
| 11.00 - 11.30 | Marco Comini, Roberta Gori, and Giorgio Levi |
How to Transform an Analyzer into a Verifier |
| 11.30 - 12.00 | Rong Yang and Steve Gregory | Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Local Search |
| Lunch | ||
| Session 20. Databases and knowledge bases | ||
| 13.30 - 14.00 | Ofer Arieli, Bert Van Nuffelen, Marc Denecker, and Maurice Bruynooghe |
Coherent composition of distributed knowledge-bases through abduction |
| 14.00 - 14.30 | Chris Fermueller, Georg Moser, and Richard Zach | Tableaux for Reasoning About Atomic Updates |
| Coffee break | ||
| Session 21. Termination | ||
| 15.00 - 15.30 | Alexander Serebrenik and Danny De Schreye | Inference of termination conditions for numerical loops in Prolog |
| 15.30 - 16.00 | Salvador Lucas | Termination of rewriting with strategy annotations |
| 16.00 - 16.30 | Samir Genaim and Michael Codish | Inferring Termination Conditions for Logic Programs using Backwards Analysis |
| Session 22. Program analysis and proof planning | ||
| 16.45 - 17.15 | Thomas Genet and Valerie Viet Triem Tong | Reachability Analysis of Term Rewriting Systems with Timbuk |
| 17.15 - 17.45 | Wim Vanhoof and Maurice Bruynooghe | Binding-time Annotations without Binding-time Analysis |
| 17.45 - 18.15 | Raul Monroy | Concept Formation via Proof Planning Failure |
