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 |