Logic for Programming, Artificial Intelligence, and Reasoning
Subtitle: 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings (Lecture Notes in Computer Science)
Contributors: Robert Nieuwenhuis (Editor); Andrei Voronkov (Editor)
Edition: 1 edition
Publisher: Springer
Published: December 18, 2001
Language: eng
Format: Paperback
Number of pages: 738
ISBN-13: 9783540429579
Subjects: Artificial Intelligence; Computer Programming; General Theory of Computing; Logic; Logic Programming; Computers; Medical / Nursing; Programming - Software Development; Computer Books: General; Programming - General; Artificial Intelligence - General; General; AI Logics; Abstraction; Automated Deduction; Automated Reasoning; Computers / Artificial Intelligence; Formal Reasoning Systems; Formal Verification; Mathematical Logic; Nonmonotonic Logics
Description: 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>