Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3--7, 2001. Proceedings. (Q1881356)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 0952.00026) Indexed articles: \textit{Hodkinson, Ian; Wolter, Frank; Zakharyaschev, Michael}, Monodic fragments of first-order temporal logics: 2000--2001 A.D., 1-23 [Zbl 1275.03088] \textit{Kupferman, Orna; Vardi, Moshe Y.}, On bounded specifications, 24-38 [Zbl 1275.68094] \textit{Schneider, Klaus}, Improving automata generation for linear temporal logic by considering the automaton hierarchy, 39-54 [Zbl 1275.68096] \textit{Diekert, Volker; Gastin, Paul}, Local temporal logic is expressively complete for cograph dependence alphabets, 55-69 [Zbl 1275.68089] \textit{Berwanger, Dietmar; Grädel, Erich}, Games and model checking for guarded logics, 70-84 [Zbl 1275.68087] \textit{Georgieva, Lilia; Hustadt, Ullrich; Schmidt, Renate A.}, Computational space efficiency and minimal model generation for guarded formulae, 85-99 [Zbl 1275.68091] \textit{Alechina, Natasha; Logan, Brian}, Logical omniscience and the cost of deliberation, 100-109 [Zbl 1275.68133] \textit{Sardiña, Sebastian}, Local conditional high-level robot programs, 110-124 [Zbl 1275.68152] \textit{Engelhardt, Kai; Van Der Meyden, Ron; Moses, Yoram}, A refinement theory that supports reasoning about knowledge and time for synchronous agents, 125-141 [Zbl 1275.68137] \textit{Letz, Reinhold; Stenz, Gernot}, Proof and model generation with disconnection tableaux, 142-156 [Zbl 1275.03081] \textit{Horton, Joseph D.}, Counting the number of equivalent binary resolution proofs, 157-171 [Zbl 1275.03080] \textit{de Nivelle, Hans}, Splitting through new proposition symbols, 172-185 [Zbl 1275.03083] \textit{Lynch, Christopher; Morawska, Barbara}, Complexity of linear standard theories, 186-200 [Zbl 1275.68127] \textit{Baaz, Matthias; Ciabattoni, Agata; Fermüller, Christian G.}, Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving, 201-216 [Zbl 1275.03098] \textit{Baader, Franz; Küsters, Ralf}, Unification in a description logic with transitive closure of roles, 217-232 [Zbl 1275.68134] \textit{Perrier, Guy}, Intuitionistic multiplicative proof nets as models of directed acyclic graph descriptions, 233-248 [Zbl 1275.03160] \textit{Luo, Yong; Luo, Zhaohui}, Coherence and transitivity in coercive subtyping, 249-265 [Zbl 1275.03077] \textit{Schürmann, Carsten}, A type-theoretic approach to induction with higher-order encodings, 266-281 [Zbl 1275.03078] \textit{Smaus, Jan-Georg}, Analysis of polymorphically typed logic programs using ACI-unification, 282-298 [Zbl 1275.68052] \textit{Koshimura, Miyuki; Fujita, Hiroshi; Hasegawa, Ryuzo}, Model generation with Boolean constraints, 299-308 [Zbl 1275.68126] \textit{Afshordel, Bijan; Hillenbrand, Thomas; Weidenbach, Christoph}, First-order atom definitions extended, 309-319 [Zbl 1275.68125] \textit{Rasmussen, Thomas Marthedal}, Automated proof support for interval logics, 320-329 [Zbl 1275.68129] \textit{Leivant, Daniel}, The functions provable by first order abstraction, 330-346 [Zbl 1234.03028] \textit{Brünnler, Kai; Tiu, Alwen Fernanto}, A local system for classical logic, 347-361 [Zbl 1275.03150] \textit{Rintanen, Jussi}, Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae, 362-376 [Zbl 1275.03082] \textit{Walsh, Toby}, Permutation problems and channelling constraints, 377-391 [Zbl 1273.68365] \textit{del Val, Alvaro}, Simplifying binary propositional theories into connected components twice as fast, 392-406 [Zbl 1275.68130] \textit{Eiter, Thomas; Fink, Michael; Sabbatini, Giuliana; Tompits, Hans}, Reasoning about evolving nonmonotonic knowledge bases, 407-421 [Zbl 1275.68136] \textit{Behrend, Andreas}, Efficient computation of the well-founded model using update propagation, 422-437 [Zbl 1275.68044] \textit{Amato, Gianluca; Lipton, James}, Indexed categories and bottom-up semantics of logic programs, 438-454 [Zbl 1275.68042] \textit{López-Fraguas, F. J.; Sánchez-Hernández, J.}, Functional logic programming with failure: a set-oriented view, 455-469 [Zbl 1275.68047] \textit{Kreutzer, Stephan}, Operational semantics for fixed-point logics on constraint databases, 470-484 [Zbl 1275.68066] \textit{Muñoz, Susana; Moreno, Juan José; Hermenegildo, Manuel}, Efficient negation using abstract interpretation, 485-494 [Zbl 1275.68049] \textit{Boulmé, Sylvain; Hamon, Grégoire}, Certifying synchrony for free, 495-506 [Zbl 1275.68057] \textit{McMath, David; Rozenfeld, Marianna; Sommer, Richard}, A computer environment for writing ordinary mathematical proofs, 507-516 [Zbl 1275.68128] \textit{Serebrenik, Alexander; De Schreye, Danny}, On termination of meta-programs, 517-530 [Zbl 1275.68050] \textit{Borralleras, Cristina; Rubio, Albert}, A monotonic higher-order semantic path ordering, 531-547 [Zbl 1275.68082] \textit{Franconi, Enrico; Palma, Antonio Laureti; Leone, Nicola; Perri, Simona; Scarcello, Francesco}, Census data repair: a challenging application of disjunctive logic programming, 561-578 [Zbl 1275.68045] \textit{Bagnara, Roberto; Zaffanella, Enea; Gori, Roberta; Hill, Patricia M.}, Boolean functions for finite-tree dependencies, 579-594 [Zbl 1275.68043] \textit{Comini, Marco; Gori, Roberta; Levi, Giorgio}, How to transform an analyzer into a verifier, 595-609 [Zbl 1275.68088] \textit{Arieli, Ofer; Van Nuffelen, Bert; Denecker, Marc; Bruynooghe, Maurice}, Coherent composition of distributed knowledge-bases through abduction, 624-638 [Zbl 1275.68064] \textit{Fermüller, Christian G.; Moser, Georg; Zach, Richard}, Tableaux for reasoning about atomic updates, 639-653 [Zbl 1275.68065] \textit{Serebrenik, Alexander; De Schreye, Danny}, Inference of termination conditions for numerical loops in Prolog, 654-669 [Zbl 1275.68051] \textit{Lucas, Salvador}, Termination of rewriting with strategy annotations, 669-684 [Zbl 1275.68084] \textit{Genaim, Samir; Codish, Michael}, Inferring termination conditions for logic programs using backwards analysis, 685-694 [Zbl 1275.68046] \textit{Genet, Thomas; Tong, Valérie Viet Triem}, Reachability analysis of term rewriting systems with Timbuk, 695-706 [Zbl 1275.68083] \textit{Vanhoof, Wim; Bruynooghe, Maurice}, Binding-time annotations without binding-time analysis, 707-722 [Zbl 1275.68053] \textit{Monroy, Raúl}, Concept formation via proof planning failure, 723-736 [Zbl 1275.68140]