7. LPAR 2000: Reunion Island, France

@proceedings{DBLP:conf/lpar/2000,
  editor    = {Michel Parigot and
               Andrei Voronkov},
  title     = {Logic for Programming and Automated Reasoning, 7th International
               Conference, LPAR 2000, Reunion Island, France, November 11-12,
               2000, Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1955},
  year      = {2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Session 1. Nonmononic reasoning

• Thomas Eiter, Georg Gottlob:
  On the Complexity of Theory Curbing. 1-19
  Electronic Edition (Springer LINK) BibTeX

Session 2. Descriptive complexity

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

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
  Electronic Edition (Springer LINK) BibTeX
• Slawomir Lasota:
  Behavioural Constructor Implementation for Regular Algebras. 54-69
  Electronic Edition (Springer LINK) BibTeX
• Thomas Hallgren, Aarne Ranta:
  An Extensible Proof Text Editor. 70-84
  Electronic Edition (Springer LINK) BibTeX
• David Delahaye:
  A Tactic Language for the System Coq. 85-95
  Electronic Edition (Springer LINK) BibTeX

Session 4. Theorem proving

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

Session 5. Verification

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

Session 6. Logic programming and CLP

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

Session 7. Nonclassical logics and lambda calculus

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

Session 8. Logic and databases

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

Session 9. Program analysis

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

Section 10. Mu-calculus

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

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
  Electronic Edition (Springer LINK) BibTeX
• Helko Lehmann, Michael Leuschel:
  Solving Planning Problems by Partial Deduction. 451-468
  Electronic Edition (Springer LINK) BibTeX
• Ján Sefránek:
  A Kripkean Semantics for Dynamic Logic Programming. 469-486
  Electronic Edition (Springer LINK) BibTeX