LPAR 2001
Logic for Programming, Aritificial Intelligence and Reasoning

Havana, Cuba, 
December 3-7, 2001

Programme

Monday, December 3

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 

Tuesday, December 4

 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 

Wednesday, December 5

 Session 11A || 11B. Discussion
 10.00 - 17.00   Discussion   LPAR 
 Session 11B || 11A. Excursion
 10.00 - 17.00   Excursion   Beach 
 Conference dinner (19:00)

Thursday, December 6

 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 

Friday, December 7

 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 

 
 

Back to the LPAR 2001 homepage