LEADER 07466nam 22008175 450 001 996466348903316 005 20200705073008.0 010 $a3-540-89439-X 024 7 $a10.1007/978-3-540-89439-1 035 $a(CKB)1000000000545845 035 $a(SSID)ssj0000318697 035 $a(PQKBManifestationID)11279924 035 $a(PQKBTitleCode)TC0000318697 035 $a(PQKBWorkID)10336029 035 $a(PQKB)10804473 035 $a(DE-He213)978-3-540-89439-1 035 $a(MiAaPQ)EBC3063747 035 $a(MiAaPQ)EBC6284317 035 $a(PPN)130186163 035 $a(EXLCZ)991000000000545845 100 $a20100301d2008 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aLogic for Programming, Artificial Intelligence, and Reasoning$b[electronic resource] $e15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Proceedings /$fedited by Iliano Cervesato, Helmut Veith, Andrei Voronkov 205 $a1st ed. 2008. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2008. 215 $a1 online resource (XIV, 714 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v5330 300 $aInternational conference proceedings. 311 $a3-540-89438-1 320 $aIncludes bibliographical references and index. 327 $aSession 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. 330 $aThis 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 carefully revised and selected from 153 submissions. The papers address all current issues in automated reasoning, computational logic, programming languages and their applications and are organized in topical sections on automata, linear arithmetic, verification knowledge representation, proof theory, quantified constraints, as well as modal and temporal logics. 410 0$aLecture Notes in Artificial Intelligence ;$v5330 606 $aArtificial intelligence 606 $aSoftware engineering 606 $aComputer programming 606 $aComputer logic 606 $aMathematical logic 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aArtificial intelligence. 615 0$aSoftware engineering. 615 0$aComputer programming. 615 0$aComputer logic. 615 0$aMathematical logic. 615 14$aArtificial Intelligence. 615 24$aSoftware Engineering/Programming and Operating Systems. 615 24$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 676 $a005.115 702 $aCervesato$b Iliano$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aVeith$b Helmut$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aVoronkov$b Andrei$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aLPAR (Conference) 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996466348903316 996 $aLogic for Programming, Artificial Intelligence, and Reasoning$9772423 997 $aUNISA