000 07055nam a22006375i 4500
001 978-3-642-14203-1
003 DE-He213
005 20240730195207.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 _aTA347.A78
072 7 _aUYQ
_2bicssc
072 7 _aCOM004000
_2bisacsh
072 7 _aUYQ
_2thema
082 0 4 _a006.3
_223
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.
250 _a1st ed. 2010.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2010.
300 _aXII, 536 p.
_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 Artificial Intelligence,
_x2945-9141 ;
_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 -- ADecision 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 volume contains the proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010). IJCAR 2010 was held during July 16-19 as part of the 2010 Federated Logic Conference, hosted by the School of Informatics at the University ofEdinburgh,Scotland. Support by the conference sponsors - EPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc. , Google, Hewlett-Packard, Intel - is gratefully acknowledged. IJCARisthepremierinternationaljointconferenceonalltopicsinautomated reasoning, including foundations, implementations, and applications. Previous IJCAR conferences were held at Siena (Italy) in 2001, Cork (Ireland) in 2004, Seattle (USA) in 2006, and Sydney (Australia) in 2008. IJCAR comprises s- eral leading conferences and workshops. In 2010, IJCAR was the fusion of the following events: -CADE: International Conference on Automated Deduction -FroCoS: International Symposium on Frontiers of Combining Systems -FTP: International Workshop on First-Order Theorem Proving - TABLEAUX: InternationalConferenceonAutomatedReasoningwith- alytic Tableaux and Related Methods There were 89 submissions (63 regular papers and 26 system descriptions) of which 40 were accepted (28 regular papers and 12 system descriptions). Each submission was assigned to at least three Program Committee members, who carefully reviewed the papers, with the help of 92 external referees. Afterwards, the submissions were discussed by the ProgramCommittee during two weeks by means of Andrei Voronkov's EasyChair system. We want to thank Andrei very much for providing his system, which was very helpful for the management of the submissions and reviews and for the discussion of the Program Committee.
650 0 _aArtificial intelligence.
_93407
650 0 _aComputer systems.
_9159458
650 0 _aComputer programming.
_94169
650 0 _aMachine theory.
_9159459
650 0 _aComputer science.
_99832
650 0 _aLogic design.
_93686
650 1 4 _aArtificial Intelligence.
_93407
650 2 4 _aComputer System Implementation.
_938514
650 2 4 _aProgramming Techniques.
_9159460
650 2 4 _aFormal Languages and Automata Theory.
_9159461
650 2 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aLogic Design.
_93686
700 1 _aGiesl, Jürgen.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9159462
700 1 _aHähnle, Reiner.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9159463
710 2 _aSpringerLink (Online service)
_9159464
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783642142024
776 0 8 _iPrinted edition:
_z9783642142048
830 0 _aLecture Notes in Artificial Intelligence,
_x2945-9141 ;
_v6173
_9159465
856 4 0 _uhttps://doi.org/10.1007/978-3-642-14203-1
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c95518
_d95518