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...
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2008.
|
| Σειρά: | Lecture Notes in Computer Science,
5330 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
