Logic for programming, artificial intelligence, and reasoning

Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR 2001 Havana, Cuba, December 3–7, 2001 Proceedings<br />Author: Robert Nieuwenhuis, Andrei Voronkov<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-42957-9<br /> DOI: 10.1007/3-540-45653-8<br /><br />Table of Contents:<p></p><ul><li>Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D. </li><li>On Bounded Specifications </li><li>Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy </li><li>Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets </li><li>Games and Model Checking for Guarded Logics </li><li>Computational Space Efficiency and Minimal Model Generation for Guarded Formulae </li><li>Logical Omniscience and the Cost of Deliberation </li><li>Local Conditional High-Level Robot Programs </li><li>A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents </li><li>Proof and Model Generation with Disconnection Tableaux </li><li>Counting the Number of Equivalent Binary Resolution Proofs </li><li>Splitting through New Proposition Symbols </li><li>Complexity of Linear Standard Theories </li><li>Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving </li><li>Unification in a Description Logic with Transitive Closure of Roles </li><li>Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions </li><li>Coherence and Transitivity in Coercive Subtyping </li><li>A Type-Theoretic Approach to Induction with Higher-Order Encodings </li><li>Analysis of Polymorphically Typed Logic Programs Using ACI-Unification </li><li>Model Generation with Boolean Constraints</li></ul>