000			06237nam a22005775i 4500
003			DE-He213
005			20191013150331.0
007			cr nn 008mamaa
008			100301s2008 gw | s |||| 0|eng d
020	6	4	_a9783540894391 _9978-3-540-89439-1
024	8	7	_a10.1007/978-3-540-89439-1 _2doi
050	8	4	_aQ334-342
050	8	4	_aTJ210.2-211.495
072	8	7	_aUYQ _2bicssc
072	8	7	_aTJFM1 _2bicssc
072	8	7	_aCOM004000 _2bisacsh
082			_a006.3 _223
100	8	1	_aCervesato, Iliano. _eeditor. _9146079
245	9	7	_aLogic for Programming, Artificial Intelligence, and Reasoning _h[electronic resource] : _b15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings / _cedited by Iliano Cervesato, Helmut Veith, Andrei Voronkov.
001			000065748
300	6	4	_aXIV, 714 p. _bonline resource.
490	8	1	_aLecture Notes in Computer Science, _x0302-9743 ; _v5330
505	8	0	_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 SystemF -- 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 Shohams Interval Temporal Logic: Towards a Complete Classification -- The Variable Hierarchy for the Lattice ?-Calculus -- A Formalised Lower Bound on UndirectedGraphReachability -- 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.
520	6	4	_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.
650	8	0	_aComputer science. _9146080
650	8	0	_aSoftware engineering. _99213
650	8	0	_aLogic design. _9146081
650	8	0	_aArtificial intelligence. _98970
650			_aComputer Science. _9146082
650			_aArtificial Intelligence (incl. Robotics). _98973
650			_aProgramming Techniques. _910862
650			_aSoftware Engineering. _99213
650			_aLogics and Meanings of Programs. _913880
650			_aMathematical Logic and Formal Languages. _910185
700	8	1	_aVeith, Helmut. _eeditor. _9146083
700	8	1	_aVoronkov, Andrei. _eeditor. _9146084
710	8	2	_aSpringerLink (Online service) _9146085
773	8	0	_tSpringer eBooks
776			_iPrinted edition: _z9783540894384
830	8	0	_aLecture Notes in Computer Science, _x0302-9743 ; _v5330 _9146086
856			_uhttp://dx.doi.org/10.1007/978-3-540-89439-1 _zde clik aquí para ver el libro electrónico
264	8	1	_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2008.
336	6	4	_atext _btxt _2rdacontent
337	6	4	_acomputer _bc _2rdamedia
338	6	4	_aonline resource _bcr _2rdacarrier
347	6	4	_atext file _bPDF _2rda
516	6	4	_aZDB-2-SCS
516	6	4	_aZDB-2-LNC
999			_c65478 _d65478
942			_c05