Automated Deduction -- CADE-24 : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings / edited by Maria Paola Bonacina.

Format:

Book

Contributor:

Bonacina, Maria Paola, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science. Lecture notes in artificial intelligence ; 7898.

Lecture Notes in Artificial Intelligence ; 7898

Language:

English

Subjects (All):

Artificial intelligence.

Logic, Symbolic and mathematical.

Computer logic.

Software engineering.

Algorithms.

Artificial Intelligence.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Algorithm Analysis and Problem Complexity.

Local Subjects:

Artificial Intelligence.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Algorithm Analysis and Problem Complexity.

Physical Description:

1 online resource (XVI, 466 pages) : 95 illustrations.

Edition:

First edition 2013.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2013.

System Details:

text file PDF

Summary:

This 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.

Contents:

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 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.

Other Format:

Printed edition:

ISBN:

978-3-642-38574-2

9783642385742

Access Restriction:

Restricted for use by site license.