000			05664nam a22005655i 4500
001			978-3-642-14203-1
003			DE-He213
005			20140220084541.0
007			cr nn 008mamaa
008			100712s2010 gw | s |||| 0|eng d
020			_a9783642142031 _9978-3-642-14203-1
024	7		_a10.1007/978-3-642-14203-1 _2doi
050		4	_aQ334-342
050		4	_aTJ210.2-211.495
072		7	_aUYQ _2bicssc
072		7	_aTJFM1 _2bicssc
072		7	_aCOM004000 _2bisacsh
082	0	4	_a006.3 _223
100	1		_aGiesl, Jürgen. _eeditor.
245	1	0	_aAutomated Reasoning _h[electronic resource] : _b5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings / _cedited by Jürgen Giesl, Reiner Hähnle.
264		1	_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2010.
300			_aXII, 534p. 85 illus. _bonline resource.
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
347			_atext file _bPDF _2rda
490	1		_aLecture Notes in Computer Science, _x0302-9743 ; _v6173
505	0		_aLogical Frameworks and Combination of Systems -- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus -- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) -- MCMT: A Model Checker Modulo Theories -- On Hierarchical Reasoning in Combinations of Theories -- Description Logic I -- Global Caching for Coalgebraic Description Logics -- Tractable Extensions of the Description Logic with Numerical Datatypes -- Higher-Order Logic -- Analytic Tableaux for Higher-Order Logic with Choice -- Monotonicity Inference for Higher-Order Formulas -- Sledgehammer: Judgement Day -- Invited Talk -- Logic between Expressivity and Complexity -- Verification -- Multi-Prover Verification of Floating-Point Programs -- Verifying Safety Properties with the TLA?+? Proof System -- MUNCH - Automated Reasoner for Sets and Multisets -- A Slice-Based Decision Procedure for Type-Based Partial Orders -- Hierarchical Reasoning for the Verification of Parametric Systems -- First-Order Logic -- Interpolation and Symbol Elimination in Vampire -- iProver-Eq: An Instantiation-Based Theorem Prover with Equality -- Classical Logic with Partial Functions -- Non-Classical Logic -- Automated Reasoning for Relational Probabilistic Knowledge Representation -- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse -- Terminating Tableaux for Hybrid Logic with Eventualities -- Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic -- Induction -- Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion -- Focused Inductive Theorem Proving -- Decision Procedures -- A Decidable Class of Nested Iterated Schemata -- RegSTAB: A SAT Solver for Propositional Schemata -- Linear Quantifier Elimination as an Abstract Decision Procedure -- A Decision Procedure for CTL* Based on Tableaux and Automata -- URBiVA: Uniform Reduction to Bit-Vector Arithmetic -- Keynote Talk -- Induction, Invariants, and Abstraction -- Arithmetic -- A Single-Significant-Digit Calculus for Semi-Automated Guesstimation -- Perfect Discrimination Graphs: Indexing Terms with Integer Exponents -- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic -- Invited Talk -- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development -- Applications -- Automating Security Analysis: Symbolic Equivalence of Constraint Systems -- System Description: The Proof Transformation System CERES -- Premise Selection in the Naproche System -- On the Saturation of YAGO -- Description Logic II -- Optimized Description Logic Reasoning via Core Blocking -- An Extension of Complex Role Inclusion Axioms in the Description Logic -- Termination -- Decreasing Diagrams and Relative Termination -- Monotonicity Criteria for Polynomial Interpretations over the Naturals -- Termination Tools in Ordered Completion.
520			_aThis book constitutes the refereed proceedings of the 5th International Joint Conference on Automated Reasoning, IJCAR 2010, held in Edinburgh, UK, in July 2010 as part of the Federated Logic Conference, FLoC 2010.The 28 revised full research papers and 12 revised system descriptions presented together with 1 full paper and 2 abstracts of invited talks were carefully reviewed and selected from 63 full paper and 26 system description submissions. The papers address the entire spectrum of research in automated reasoning and are organized in topical sections on logical frameworks and combination of systems; description logic; higher-order logic; verification; first-order logic; non-classical logic; induction; decision procedures; arithmetic; applications; and termination.
650		0	_aComputer science.
650		0	_aLogic design.
650		0	_aComputational complexity.
650		0	_aArtificial intelligence.
650	1	4	_aComputer Science.
650	2	4	_aArtificial Intelligence (incl. Robotics).
650	2	4	_aMathematical Logic and Formal Languages.
650	2	4	_aLogics and Meanings of Programs.
650	2	4	_aLogic Design.
650	2	4	_aDiscrete Mathematics in Computer Science.
650	2	4	_aMathematics of Computing.
700	1		_aHähnle, Reiner. _eeditor.
710	2		_aSpringerLink (Online service)
773	0		_tSpringer eBooks
776	0	8	_iPrinted edition: _z9783642142024
830		0	_aLecture Notes in Computer Science, _x0302-9743 ; _v6173
856	4	0	_uhttp://dx.doi.org/10.1007/978-3-642-14203-1
912			_aZDB-2-SCS
912			_aZDB-2-LNC
999			_c112430 _d112430