Logic for Programming, Artificial Intelligence, and Reasoning 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Proceedings /
This book constitutes the refereed proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008, which took place in Doha, Qatar, during November 22-27, 2008. The 45 revised full papers presented together with 3 invited talks were caref...
Corporate Author: | |
---|---|
Other Authors: | , , |
Language: | English |
Published: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2008.
|
Edition: | 1st ed. 2008. |
Series: | Lecture Notes in Artificial Intelligence ;
5330 |
Subjects: | |
Online Access: | https://doi.org/10.1007/978-3-540-89439-1 |
Table of Contents:
- Session 1. Constraint Solving
- Symmetry Breaking for Maximum Satisfiability
- Efficient Generation of Unsatisfiability Proofs and Cores in SAT
- Justification-Based Local Search with Adaptive Noise Strategies
- The Max-Atom Problem and Its Relevance
- Session 2. Knowledge Representation 1
- Towards Practical Feasibility of Core Computation in Data Exchange
- Data-Oblivious Stream Productivity
- Reasoning about XML with Temporal Logics and Automata
- Distributed Consistency-Based Diagnosis
- Session 3. Proof-Theory 1
- From One Session to Many: Dynamic Tags for Security Protocols
- A Conditional Logical Framework
- Nominal Renaming Sets
- Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
- Invited Talk
- Model Checking – My 27-Year Quest to Overcome the State Explosion Problem
- Session 4. Automata
- On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata
- Recurrent Reachability Analysis in Regular Model Checking
- Alternation Elimination by Complementation (Extended Abstract)
- Discounted Properties of Probabilistic Pushdown Automata
- Session 5. Linear Arithmetic
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
- Session 6. Verification
- On Bounded Reachability of Programs with Set Comprehensions
- Program Complexity in Hierarchical Module Checking
- Valigator: A Verification Tool with Bound and Invariant Generation
- Reveal: A Formal Verification Tool for Verilog Designs
- Invited Talks
- A Formal Language for Cryptographic Pseudocode
- Reasoning Using Knots
- Session 7. Knowledge Representation 2
- Role Conjunctions in Expressive Description Logics
- Default Logics with Preference Order: Principles and Characterisations
- On Computing Constraint Abduction Answers
- Fast Counting with Bounded Treewidth
- Session 8. Proof-Theory 2
- Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
- Focusing Strategies in the Sequent Calculus of Synthetic Connectives
- An Algorithmic Interpretation of a Deep Inference System
- Weak ??-Normalization and Normalization by Evaluation for System F
- Session 9. Quantified Constraints
- Variable Dependencies of Quantified CSPs
- Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings
- Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates
- A Logic of Singly Indexed Arrays
- Session 10. Modal and Temporal Logics
- On the Computational Complexity of Spatial Logics with Connectedness Constraints
- Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification
- The Variable Hierarchy for the Lattice ?-Calculus
- A Formalised Lower Bound on Undirected Graph Reachability
- Session 11. Rewriting
- Improving Context-Sensitive Dependency Pairs
- Complexity, Graphs, and the Dependency Pair Method
- Uncurrying for Termination
- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
- A Higher-Order Iterative Path Ordering
- Variable Dependencies of Quantified CSPs.