LPAR 2002
Logic for Programming, Aritificial Intelligence and Reasoning

Tbilisi, Georgia
October 14-18, 2002

Monday, October 14

Session 1
 10:00 - 10:30   J. Siekmann, C. Benzmüller, A. Fiedler,
 A. Meier, and M. Pollet
 Proof Development With Omega: sqrt{2} is Irrational
 10:30 - 11:00   Claudio Castellini and Alan Smaill  Proof Planning for Feature Interactions:
 a Preliminary Report
 11:00 - 11:30   Julian Richardson  A Semantics for Proof Plans with Applications
 to Interactive Proof Planning
  Coffee break
Session 2
 12:00 - 12:30   AK McIver and CC Morgan  Games, Probability and the Quantitative mu-Calculus
 12:30 - 13:00   Pascal Fontaine and E. Pascal Gribomont  Using BDDs with Combinations of Theories
  Lunch
Session 3: invited talk
 14:30 - 15:30   Kostic Sagonas  Tabling in Logic Programming and its Implementations
  Coffee break
Session 4
 16:00 - 16:30   James Brotherston,
 Anatoli Degtyarev,
 Michael Fisher, and Alexei Lisitsa
 Searching for Invariants Using Temporal Resolution
 16:30 - 17:00   Temur Kutsia  Theorem Proving with Sequence Variables and
 Flexible Arity Symbols
 17:00 - 17:30   Sergio Tessaris and Ian Horrocks  Abox Satisfiability Reduced to Terminological
 Reasoning in Expressive Description Logics
 17:30 - 18:00   Fabio Grandi  On Expressive Description Logics with Composition
 of Roles in Number Restrictions
  19:00 Conference dinner

Tuesday, October 15

Session 5
 9:30 - 10:00   Jose Espirito Santo  An Isomorphism Between a Fragment of Sequent
 Calculus and an Extension of Natural Deduction
 10:00 - 10:30   Stefan Edelkamp and Peter Leven  Directed Automated Theorem Proving
 10:30 - 11:00   Lutz Strassburger  A Local System for Linear Logic
  Coffee break
Session 6
 11:30 - 12:00   Martin Strecker  Investigating Type-Certifying Compilation with Isabelle
 12:00 - 12:30   Don Syme and Andrew D. Gordon  Automating Type Soundness Proofs via
 Decision Procedures and Guided Reductions
 12:30 - 13:00   M. Alpuente, S. Escobar,
 B. Gramlich, and S. Lucas
 Improving On-Demand Strategy Annotations
  Lunch
Session 7: invited talk
 14:30 - 15:30   Christian Fermüller  Parallel Dialogue Games for Intermediate Logics
  Coffee break
Session 8
 16:00 - 16:30   Norbert Preining  Gödel Logics and Cantor-Bendixon Analysis
 16:30 - 17:00   K. R. Apt and C. F. M. Vermeulen  First-Order Logic as a Constraint
 Programming Language
 17:00 - 17:30   Joachim Niehren and Mateu Villaret  Parallelism and Tree Regular Constraints
 17:30 - 18:00   Arnold Beckmann  A Note on Universal Measures for Weak
 Implicit Computational Complexity

Wednesday, October 16

If weather permits, we will visit the village Kasbegi driving along the famous "Georgian Military Road" constructed in the 19th century. This gives us the possibility to see the awesome mountain range of High Caucasus from short distance. We will visit the famous church on the slopes of Mount Kasbegi, the king of Caucasus (second highest mountain after Elbrus). On the way we will have the opportunity to visit several castles and churches, including the churches of Mxeta, the ancient capital of Georgia.

The excursion will be followed by a barbecue until late in the night.

Thursday, October 17

Session 9
 9:30 - 10:00   Benedikt Bollig, Martin Leucker,
 and Philipp Lucas
 Extending Compositional Message Sequence Graphs
 10:00 - 10:30   Gilles Dowek, Therese Hardin
 and Clause Kirchner
 Binding Logic: Proofs and Models
 10:30 - 11:00   Mehdi Dastani and Leendert
 van der Torre
 An Extension of BDI-CTL with Functional
 Dependencies and Components
  Coffee break
Session 10
 11:30 - 12:00   Serge Autexier and Dieter Hutter  Maintenance of Formal Software Developments
 by Stratified Verification
 12:00 - 12:30   Alessio Guglielmi and Lutz Strassburger  A Non-Commutative Extension of MELL
 12:30 - 13:00   Mauro Ferrari, Camillo Fiorentini, and
 Guido Fiorino
 On the Complexity of Disjunction and Explicit
 Definability Properties in Some Intermediate Logics
  Lunch
Session 11
 14:30 - 15:00   Gianluigi Greco, Sergio Greco, Irina
 Trubtsyna, and Ester Zumpano
 Query Optimization of Disjunctive Databases with
 Constraints Through Binding Propagation
 15:00 - 15:30   Claudio Vaucheret, Sergio Guadarrama,
 and Susana Munoz
 Fuzzy Prolog: a Simple General Implementation
 Using CLP(R)
 15:30 - 16:00   Orna Kupferman, Nir Piterman, and
 Moshe Y. Vardi
 Pushdown Specifications

Friday, October 18

Workshop and poster session

The Friday programme will consist of:

running in parallel. The workshop programme is available at the workshop programme page The poster session programme is given below and scheduled so as not to interfere with the invited talks of the workshop.

Social program

There will be an overview excursion of Tbilisi followed by a dinner in a (nice) restaurant in Tbilisi until very late. The excursion will start at 17:00, immediately after the last workshop talk.

Friday, October 18. Poster session

Session A
 10:35 - 10:40   Tanel Tammet  Efficient finite model building using the Mace algorithm
and non-ground splitting
 10:40 - 10:45   Anna Romina  TBA
 10:45 - 10:50   Konstantin Pkhakadze and M. Ivanishvili  Towards the Strong Formal Logic Understanding
of the Word Based on the Natural Georgian Language System
 10:50 - 10:55   Khimuri Rukhaia and Lali Tibua  A Problem in Mechanical Theorem Proving
  Coffee break
 11:15 - 11:20   Juan Heguiabehere  Pre- and Postcondition Reasoning in Dynamic First Order Logic
 11:20 - 11:25   Alessandro Avellone, Guido Fiorino,
 Ugo Moscato.
 A new O(n log n)-SPACE decision procedure for
 propositional intuitionistic logic
 11:25 - 12:30     Posters