Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings

Front Matter....Pages -
Symmetry Breaking for Maximum Satisfiability....Pages 1-15
Efficient Generation of Unsatisfiability Proofs and Cores in SAT....Pages 16-30
Justification-Based Local Search with Adaptive Noise Strategies....Pages 31-46
The Max-Atom Problem and Its Relevance....Pages 47-61
Towards Practical Feasibility of Core Computation in Data Exchange....Pages 62-78
Data-Oblivious Stream Productivity....Pages 79-96
Reasoning about XML with Temporal Logics and Automata....Pages 97-112
Distributed Consistency-Based Diagnosis....Pages 113-127
From One Session to Many: Dynamic Tags for Security Protocols....Pages 128-142
A Conditional Logical Framework....Pages 143-157
Nominal Renaming Sets....Pages 158-173
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic....Pages 174-181
Model Checking – My 27-Year Quest to Overcome the State Explosion Problem....Pages 182-182
On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata....Pages 183-197
Recurrent Reachability Analysis in Regular Model Checking....Pages 198-213
Alternation Elimination by Complementation (Extended Abstract)....Pages 214-229
Discounted Properties of Probabilistic Pushdown Automata....Pages 230-242
A Quantifier Elimination Algorithm for Linear Real Arithmetic....Pages 243-257
 (LIA) - Model Evolution with Linear Integer Arithmetic Constraints....Pages 258-273
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic....Pages 274-289
Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking....Pages 290-304
On Bounded Reachability of Programs with Set Comprehensions....Pages 305-317
Program Complexity in Hierarchical Module Checking....Pages 318-332
 Valigator : A Verification Tool with Bound and Invariant Generation....Pages 333-342
Reveal: A Formal Verification Tool for Verilog Designs....Pages 343-352
A Formal Language for Cryptographic Pseudocode....Pages 353-376
Reasoning Using Knots....Pages 377-390
Role Conjunctions in Expressive Description Logics....Pages 391-405
Default Logics with Preference Order: Principles and Characterisations....Pages 406-420
On Computing Constraint Abduction Answers....Pages 421-435
Fast Counting with Bounded Treewidth....Pages 436-450
Cut Elimination for First Order Gödel Logic by Hyperclause Resolution....Pages 451-466
Focusing Strategies in the Sequent Calculus of Synthetic Connectives....Pages 467-481
An Algorithmic Interpretation of a Deep Inference System....Pages 482-496
Weak βη -Normalization and Normalization by Evaluation for System F....Pages 497-511
Variable Dependencies of Quantified CSPs....Pages 512-527
Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings....Pages 528-542
Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates....Pages 543-557
A Logic of Singly Indexed Arrays....Pages 558-573
On the Computational Complexity of Spatial Logics with Connectedness Constraints....Pages 574-589
Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification....Pages 590-604
The Variable Hierarchy for the Lattice μ -Calculus....Pages 605-620
A Formalised Lower Bound on Undirected Graph Reachability....Pages 621-635
Improving Context-Sensitive Dependency Pairs....Pages 636-651
Complexity, Graphs, and the Dependency Pair Method....Pages 652-666
Uncurrying for Termination....Pages 667-681
Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation....Pages 682-696
A Higher-Order Iterative Path Ordering....Pages 697-711
Variable Dependencies of Quantified CSPs....Pages E1-E1
Back Matter....Pages -