Automated Deduction -- CADE-24

24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings

AvMaria Paola Bonacina

Häftad, Engelska, 2013

Del i serien Lecture Notes in Computer Science

550 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

This book constitutes the proceedings of the 24th International Conference on Automated Deduction, CADE-24, held in Lake Placid, NY, USA, in June 2013.

Produktinformation

Utgivningsdatum:2013-05-16
Mått:155 x 235 x 27 mm
Vikt:727 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:466
Upplaga:2013
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783642385735

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Programvaruutveckling inom Data och IT
Artificiell intelligens inom Data och IT

Innehållsförteckning

One 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 andRelation 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 Applicationto 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 CryptographicProtocol 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.