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