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...

Full description

Corporate Author: SpringerLink (Online service)
Other Authors: Cervesato, Iliano. (Editor, http://id.loc.gov/vocabulary/relators/edt), Veith, Helmut. (Editor, http://id.loc.gov/vocabulary/relators/edt), Voronkov, Andrei. (Editor, http://id.loc.gov/vocabulary/relators/edt)
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.