CADE 2013 - LNAI 7898

Maria Paola Bonacina (Ed.):

Automated Deduction – CADE-24

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

LNAI 7898

Ordering Information

BibTeX

Title Pages in PDF
Preface in PDF
Organization in PDF
Table of Contents in PDF

One Logic to Use Them All
Jean-Christophe Filliâtre
LNAI 7898, p. 1 ff.
Abstract | Full article in PDF | BibTeX

The Tree Width of Separation Logic with Recursive Definitions
Radu Iosif, Adam Rogalewicz, and Jiri Simacek
LNAI 7898, p. 21 ff.
Abstract | Full article in PDF | BibTeX

Hierarchic Superposition with Weak Abstraction
Peter Baumgartner and Uwe Waldmann
LNAI 7898, p. 39 ff.
Abstract | Full article in PDF | BibTeX

Completeness and Decidability Results for First-Order Clauses with Indices
Abdelkader Kersani and Nicolas Peltier
LNAI 7898, p. 58 ff.
Abstract | Full article in PDF | BibTeX

A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
Marta Cialdea Mayer
LNAI 7898, p. 76 ff.
Abstract | Full article in PDF | BibTeX

Tractable Inference Systems: An Extension with a Deducibility Predicate
Hubert Comon-Lundh, Véronique Cortier, and Guillaume Scerri
LNAI 7898, p. 91 ff.
Abstract | Full article in PDF | BibTeX

Computing Tiny Clause Normal Forms
Noran Azmy and Christoph Weidenbach
LNAI 7898, p. 109 ff.
Abstract | Full article in PDF | BibTeX

System Description: E-KRHyper 1.4
Markus Bender, Björn Pelzer, and Claudia Schon
LNAI 7898, p. 126 ff.
Abstract | Full article in PDF | BibTeX

Analysing Vote Counting Algorithms via Logic
Bernhard Beckert, Rajeev Goré, and Carsten Schürmann
LNAI 7898, p. 135 ff.
Abstract | Full article in PDF | BibTeX

Automated Reasoning, Fast and Slow
Natarajan Shankar
LNAI 7898, p. 145 ff.
Abstract | Full article in PDF | BibTeX

Foundational Proof Certificates in First-Order Logic
Zakaria Chihani, Dale Miller, and Fabien Renaud
LNAI 7898, p. 162 ff.
Abstract | Full article in PDF | BibTeX

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
Leonardo de Moura and Grant Olney Passmore
LNAI 7898, p. 178 ff.
Abstract | Full article in PDF | BibTeX

A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, and Bernd Becker
LNAI 7898, p. 193 ff.
Abstract | Full article in PDF | BibTeX

dReal: An SMT Solver for Nonlinear Theories over the Reals
Sicun Gao, Soonho Kong, and Edmund M. Clarke
LNAI 7898, p. 208 ff.
Abstract | Full article in PDF | BibTeX

Solving Difference Constraints over Modular Arithmetic
Graeme Gange, Harald Søndergaard, Peter J. Stuckey, and Peter Schachte
LNAI 7898, p. 215 ff.
Abstract | Full article in PDF | BibTeX

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher A. Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse
LNAI 7898, p. 231 ff.
Abstract | Full article in PDF | BibTeX

Hierarchical Combination
Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen
LNAI 7898, p. 249 ff.
Abstract | Full article in PDF | BibTeX

PRocH: Proof Reconstruction for HOL Light
Cezary Kaliszyk and Josef Urban
LNAI 7898, p. 267 ff.
Abstract | Full article in PDF | BibTeX

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description
Rajeev Goré and Jimmy Thomson
LNAI 7898, p. 275 ff.
Abstract | Full article in PDF | BibTeX

Towards Modularly Comparing Programs Using Automated Theorem Provers
Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebêlo
LNAI 7898, p. 282 ff.
Abstract | Full article in PDF | BibTeX

Reuse in Software Verification by Abstract Method Calls
Reiner Hähnle, Ina Schaefer, and Richard Bubel
LNAI 7898, p. 300 ff.
Abstract | Full article in PDF | BibTeX

Dynamic Logic with Trace Semantics
Bernhard Beckert and Daniel Bruns
LNAI 7898, p. 315 ff.
Abstract | Full article in PDF | BibTeX

Temporalizing Ontology-Based Data Access
Franz Baader, Stefan Borgwardt, and Marcel Lippmann
LNAI 7898, p. 330 ff.
Abstract | Full article in PDF | BibTeX

Verifying Refutations with Extended Resolution
Marijn J.H. Heule, Warren A. Hunt Jr., and Nathan Wetzler
LNAI 7898, p. 345 ff.
Abstract | Full article in PDF | BibTeX

Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
Viorica Sofronie-Stokkermans
LNAI 7898, p. 360 ff.
Abstract | Full article in PDF | BibTeX

Quantifier Instantiation Techniques for Finite Model Finding in SMT
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krsti, Morgan Deters, and Clark Barrett
LNAI 7898, p. 377 ff.
Abstract | Full article in PDF | BibTeX

Automating Inductive Proofs Using Theory Exploration
Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone
LNAI 7898, p. 392 ff.
Abstract | Full article in PDF | BibTeX

E-MaLeS 1.1
Daniel Kühlwein, Stephan Schulz, and Josef Urban
LNAI 7898, p. 407 ff.
Abstract | Full article in PDF | BibTeX

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
Jasmin Christian Blanchette and Andrei Paskevich
LNAI 7898, p. 414 ff.
Abstract | Full article in PDF | BibTeX

Propositional Temporal Proving with Reductions to a SAT Problem
Richard Williams and Boris Konev
LNAI 7898, p. 421 ff.
Abstract | Full article in PDF | BibTeX

InKreSAT: Modal Reasoning via Incremental Reduction to SAT
Mark Kaminski and Tobias Tebbi
LNAI 7898, p. 436 ff.
Abstract | Full article in PDF | BibTeX

: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into
Gergely Kovásznai, Andreas Fröhlich, and Armin Biere
LNAI 7898, p. 443 ff.
Abstract | Full article in PDF | BibTeX

The 481 Ways to Split a Clause and Deal with Propositional Variables
Kryštof Hoder and Andrei Voronkov
LNAI 7898, p. 450 ff.
Abstract | Full article in PDF | BibTeX

Author Index
LNAI 7898, p. 465 f.
Author Index in PDF

Complete Volume in BibTeX