7. LPAR 2000: Reunion Island, France

Session 1. Nonmononic reasoning

• Thomas Eiter, Georg Gottlob:
  On the Complexity of Theory Curbing. 1-19
  

Session 2. Descriptive complexity

• Bruno Courcelle:
  Graph Operations and Monadic Second-Order Logic: A Survey. 20-24
  
• Jean-Yves Marion, Jean-Yves Moyen:
  Efficient First Order Functional Program Interpreter with Time Bound Certifications. 25-42
  

Session 3. Specification and automatic proof-assistants

• Wolfgang Grieskamp, Markus Lepper:
  Encoding Temporal Logics in Executable Z: A Case Study for the ZETA System. 43-53
  
• Slawomir Lasota:
  Behavioural Constructor Implementation for Regular Algebras. 54-69
  
• Thomas Hallgren, Aarne Ranta:
  An Extensible Proof Text Editor. 70-84
  
• David Delahaye:
  A Tactic Language for the System Coq. 85-95
  

Session 4. Theorem proving

• Miyuki Koshimura, Ryuzo Hasegawa:
  Proof Simplification for Model Generation and Its Applications. 96-113
  
• Christian G. Fermüller, Georg Moser:
  Have Spass with OCC1N_g⁼. 114-130
  

Session 5. Verification

• Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron:
  Compiling and Verifying Security Protocols. 131-160
  
• Jan Friso Groote, Jaco van de Pol:
  Equational Binary Decision Diagrams. 161-178
  
• Cécile Canovas-Dumas, Paul Caspi:
  A PVS Proof Obligation Generator for Lustre Programs. 179-188
  

Session 6. Logic programming and CLP

• Roberto Bagnara, Patricia M. Hill, Enea Zaffanella:
  Efficient Structural Information Analysis for Real CLP Languages. 189-206
  
• Jean-Vincent Loddo, Roberto Di Cosmo:
  Playing Logic Programs with the Alpha-Beta Algorithm. 207-224
  
• Nikolay Pelov, Emmanuel De Mot, Marc Denecker:
  Logic Programming Approaches for Representing and Solving Constraint Satisfaction Problems: A Comparison. 225-239
  

Session 7. Nonclassical logics and lambda calculus

• Matthias Baaz, Agata Ciabattoni, Richard Zach:
  Quantified Propositional Gödel Logics. 240-256
  
• Philippe de Groote:
  Proof-Search in Implicative Linear Logic as a Matching Problem. 257-274
  
• Dieter Spreen:
  A New Model Construction for the Polymorphic Lambda Calculus. 275-292
  
• Richard Statman:
  Church's Lambda Delta Calculus. 293-307
  

Session 8. Logic and databases

• Sergio Greco, Ester Zumpano:
  Querying Inconsistent Databases. 308-325
  
• Ian Horrocks, Ulrike Sattler, Sergio Tessaris, Stephan Tobies:
  How to Decide Query Containment Under Constraints Using a Description Logic. 326-343
  

Session 9. Program analysis

• Gilles Barthe, Bernard P. Serpette:
  Static Reduction Analysis for Imperative Object Oriented Languages. 344-361
  
• Roberta Gori:
  An Abstract Interpretation Approach to Termination of Logic Programs. 362-380
  
• Elvira Albert, Michael Hanus, Germán Vidal:
  Using an Abstract Representation to Specialize Functional Logic Programs. 381-398
  
• Wim Vanhoof:
  Binding-Time Analysis by Constraint Solving. A Modular and Higher-Order Approach for Mercury. 399-416
  

Section 10. Mu-calculus

• Erich Grädel:
  Efficient Evaluation Methods for Guarded Logics and Datalog LITE. 417
  
• Jean-Marc Talbot:
  On the Alternation-Free Horn Mu-calculus. 418-435
  

Session 11. Planning and reasoning about actions

• Steffen Hölldobler, Dietrich Kuske:
  The Boundary between Decidable and Undecidable Fragments of the Fluent Calculus. 436-450
  
• Helko Lehmann, Michael Leuschel:
  Solving Planning Problems by Partial Deduction. 451-468
  
• Ján Sefránek:
  A Kripkean Semantics for Dynamic Logic Programming. 469-486