LEADER 06159nam 22008775 450 001 9910483964403321 005 20200706145339.0 010 $a3-642-38574-5 024 7 $a10.1007/978-3-642-38574-2 035 $a(CKB)2560000000105649 035 $a(Springer)9783642385742 035 $a(MH)013717687-2 035 $a(SSID)ssj0000936367 035 $a(PQKBManifestationID)11469436 035 $a(PQKBTitleCode)TC0000936367 035 $a(PQKBWorkID)10974166 035 $a(PQKB)10771470 035 $a(DE-He213)978-3-642-38574-2 035 $a(MiAaPQ)EBC3093055 035 $a(PPN)170492362 035 $a(EXLCZ)992560000000105649 100 $a20130605d2013 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Deduction -- CADE-24 $e24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings /$fedited by Maria Paola Bonacina 205 $a1st ed. 2013. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2013. 215 $a1 online resource (XVI, 466 p. 95 illus.)$cdigital 225 1 $aLecture Notes in Artificial Intelligence ;$v7898 300 $aInternational conference proceedings. 311 $a3-642-38573-7 320 $aIncludes bibliographical references and index. 327 $aOne Logic to Use Them All -- The Tree Width of Separation Logic with Recursive Definitions -- Hierarchic Superposition with Weak Abstraction -- Completeness and Decidability Results for First-Order Clauses with Indices -- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies -- Tractable Inference Systems: An Extension with a Deducibility Predicate -- Computing Tiny Clause Normal Forms -- System Description: E-KRHyper 1.4 Extensions for Unique Names and Description Logic -- Analysing Vote Counting Algorithms via Logic: And Its Application to the CADE Election Scheme -- Automated Reasoning, Fast and Slow -- Foundational Proof Certificates in First-Order Logic -- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals -- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition -- dReal: An SMT Solver for Nonlinear Theories over the Reals -- Solving Difference Constraints over Modular Arithmetic -- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis -- Hierarchical Combination -- PRocH: Proof Reconstruction for HOL Light -- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description -- Towards Modularly Comparing Programs Using Automated Theorem Provers -- Reuse in Software Verification by Abstract Method Calls -- Dynamic Logic with Trace Semantics -- Temporalizing Ontology-Based Data Access -- Verifying Refutations with Extended Resolution -- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems -- Quantifier Instantiation Techniques for Finite Model Finding in SMT -- Automating Inductive Proofs Using Theory Exploration -- E-MaLeS 1.1 -- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism -- Propositional Temporal Proving with Reductions to a SAT Problem -- InKreSAT: Modal Reasoning via Incremental Reduction to SAT -- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR -- The 481 Ways to Split a Clause and Deal with Propositional Variables. 330 $aThis book constitutes the proceedings of the 24th International Conference on Automated Deduction, CADE-24, held in Lake Placid, NY, USA, in June 2013. The 31 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 71 initial submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, ranging from theoretical and methodological issues to the presentation of new theorem provers, solvers and systems. 410 0$aLecture Notes in Artificial Intelligence ;$v7898 606 $aArtificial intelligence 606 $aMathematical logic 606 $aComputer logic 606 $aSoftware engineering 606 $aAlgorithms 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aAlgorithm Analysis and Problem Complexity$3https://scigraph.springernature.com/ontologies/product-market-codes/I16021 608 $aKongress$zLake Placid, NY$y2013. 608 $aConference papers and proceedings.$2fast 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 0$aAlgorithms. 615 14$aArtificial Intelligence. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aAlgorithm Analysis and Problem Complexity. 676 $a511.3 686 $a004$2sdnb 686 $a510$2sdnb 686 $aDAT 706f$2stub 686 $aDAT 716f$2stub 686 $aSS 4800$2rvk 702 $aBonacina$b Maria Paola$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Automated Deduction 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483964403321 996 $aAutomated Deduction -- CADE-24$92593520 997 $aUNINA 999 $aThis Record contains information from the Harvard Library Bibliographic Dataset, which is provided by the Harvard Library under its Bibliographic Dataset Use Terms and includes data made available by, among others the Library of Congress