Logic for programming and automated reasoning. 7th international conference, LPAR 2000, Reunion Island, France, November 6--10, 2000. Proceedings (Q1589868)

The articles of this volume will be reviewed individually. The preceding conference (6th, 1999) has been reviewed (see Zbl 0921.00037). Indexed articles: \textit{Eiter, Thomas; Gottlob, Georg}, On the complexity of theory curbing, 1-19 [Zbl 0988.68176] \textit{Courcelle, Bruno}, Graph operations and monadic second-order logic: A survey, 20-24 [Zbl 0988.68559] \textit{Marion, Jean-Yves; Moyen, J.-Y.}, Efficient first order functional program interpreter with time bound certifications, 25-42 [Zbl 0988.68043] \textit{Grieskamp, Wolfgang; Lepper, Markus}, Encoding temporal logics in executable Z: A case study for the ZETA system, 43-53 [Zbl 0988.68563] \textit{Lasota, Sławomir}, Behavioural constructor implementation for regular algebras, 54-69 [Zbl 0988.68110] \textit{Hallgren, Thomas; Ranta, Aarne}, An extensible proof text editor, 70-84 [Zbl 0988.68586] \textit{Delahaye, David}, A tactic language for the system Coq, 85-95 [Zbl 0988.68584] \textit{Koshimura, Miyuki; Hasegawa, Ryuzo}, Proof simplification for model generation and its applications, 96-113 [Zbl 0988.68165] \textit{Fermüller, Christian G.; Moser, Georg}, Have SPASS with \(OCC1N_g^=\), 114-130 [Zbl 0988.68163] \textit{Jacquemard, Florent; Rusinowitch, Michaël; Vigneron, Laurent}, Compiling and verifying security protocols, 131-160 [Zbl 0988.68562] \textit{Groote, Jan Friso; van de Pol, Jaco}, Equational binary decision diagrams, 161-178 [Zbl 0988.68590] \textit{Canovas-Dumas, Cécile; Caspi, Paul}, A PVS proof obligation generator for Lustre programs, 179-188 [Zbl 0988.68539] \textit{Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea}, Efficient structural information analysis for real CLP languages, 189-206 [Zbl 0988.68035] \textit{Loddo, Jean-Vincent; Di Cosmo, Roberto}, Playing logic programs with the Alpha-Beta algorithm, 207-224 [Zbl 0988.68036] \textit{Pelov, Nikolay; De Mot, Emmanuel; Denecker, Marc}, Logic programming approaches for representing and solving constraint satisfaction problems: A comparison, 225-239 [Zbl 0988.68522] \textit{Baaz, Matthias; Ciabattoni, Agata; Zach, Richard}, Quantified propositional Gödel logics, 240-256 [Zbl 0988.03014] \textit{de Groote, Philippe}, Proof-search in implicative linear logic as a matching problem, 257-274 [Zbl 0988.03090] \textit{Spreen, Dieter}, A new model construction for the polymorphic lambda calculus, 275-292 [Zbl 0988.03026] \textit{Statman, Rick}, Church's lambda delta calculus, 293-307 [Zbl 0988.03027] \textit{Greco, Sergio; Zumpano, Ester}, Querying inconsistent databases, 308-325 [Zbl 0988.68061] \textit{Horrocks, Ian; Sattler, Ulrike; Tessaris, Sergio; Tobies, Stephan}, How to decide query containment under constraints using a description logic, 326-343 [Zbl 0988.68060] \textit{Barthe, Gilles; Serpette, Bernard Paul}, Static reduction analysis for imperative object oriented languages, 344-361 [Zbl 0988.68535] \textit{Gori, Roberta}, An abstract interpretation approach to termination of logic programs, 362-380 [Zbl 0988.68033] \textit{Albert, Elvira; Hanus, Michael; Vidal, Germán}, Using an abstract representation to specialize functional logic programs, 381-398 [Zbl 0988.68516] \textit{Vanhoof, Wim}, Binding-time analysis by constraint solving. A modular and higher-order approach for Mercury, 399-416 [Zbl 0988.68519] \textit{Grädel, Erich}, Efficient evaluation methods for guarded logics and Datalog LITE (abstract), 417 [Zbl 0988.68690] \textit{Talbot, Jean-Marc}, On the alternation-free Horn \(\mu\)-calculus, 418-435 [Zbl 0988.03052] \textit{Hölldobler, Steffen; Kuske, Dietrich}, The boundary between decidable and undecidable fragments of the fluent calculus, 436-450 [Zbl 0988.68179] \textit{Lehmann, Helko; Leuschel, Michael}, Solving planning problems by partial deduction, 451-468 [Zbl 0988.68177] \textit{Šefránek, Ján}, A Kripkean semantics for dynamic logic programming, 469-486 [Zbl 0988.68030]