@proceedings{LNAI7898,
   editor     = {Maria Paola Bonacina},
   title      = {Automated Deduction -- CADE-24},
   shorttitle = {CADE 2013},
   publisher  = {Springer},
   location   = {Heidelberg},
   series     = {Lecture Notes in Computer Science},
   volume     = {7898},
   year       = {2013},
   isbn       = {978-3-642-38573-5}
}

@inproceedings{LNAI78980001,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Jean-Christophe Filli\^{a}tre},
   title     = {One Logic to Use Them All},
   pages     = {1--20}
}

@inproceedings{LNAI78980021,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Radu Iosif and Adam Rogalewicz and Jiri Simacek},
   title     = {The Tree Width of Separation Logic with Recursive Definitions},
   pages     = {21--38}
}

@inproceedings{LNAI78980039,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Peter Baumgartner and Uwe Waldmann},
   title     = {Hierarchic Superposition with Weak Abstraction},
   pages     = {39--57}
}

@inproceedings{LNAI78980058,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Abdelkader Kersani and Nicolas Peltier},
   title     = {Completeness and Decidability Results for First-Order Clauses with Indices},
   pages     = {58--75}
}

@inproceedings{LNAI78980076,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Marta Cialdea Mayer},
   title     = {A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies},
   pages     = {76--90}
}

@inproceedings{LNAI78980091,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Hubert Comon-Lundh and V\'{e}ronique Cortier and Guillaume Scerri},
   title     = {Tractable Inference Systems: An Extension with a Deducibility Predicate},
   pages     = {91--108}
}

@inproceedings{LNAI78980109,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Noran Azmy and Christoph Weidenbach},
   title     = {Computing Tiny Clause Normal Forms},
   pages     = {109--125}
}

@inproceedings{LNAI78980126,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Markus Bender and Bj\"{o}rn Pelzer and Claudia Schon},
   title     = {System Description: E-KRHyper 1.4},
   pages     = {126--134}
}

@inproceedings{LNAI78980135,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Bernhard Beckert and Rajeev Gor\'{e} and Carsten Sch\"{u}rmann},
   title     = {Analysing Vote Counting Algorithms via Logic},
   pages     = {135--144}
}

@inproceedings{LNAI78980145,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Natarajan Shankar},
   title     = {Automated Reasoning, Fast and Slow},
   pages     = {145--161}
}

@inproceedings{LNAI78980162,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Zakaria Chihani and Dale Miller and Fabien Renaud},
   title     = {Foundational Proof Certificates in First-Order Logic},
   pages     = {162--177}
}

@inproceedings{LNAI78980178,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Leonardo de Moura and Grant Olney Passmore},
   title     = {Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals},
   pages     = {178--192}
}

@inproceedings{LNAI78980193,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Ulrich Loup and Karsten Scheibler and Florian Corzilius and Erika \'{A}brah\'{a}m and Bernd Becker},
   title     = {A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition},
   pages     = {193--207}
}

@inproceedings{LNAI78980208,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Sicun Gao and Soonho Kong and Edmund M. Clarke},
   title     = {{\sf dReal}: An SMT Solver for Nonlinear Theories over the Reals},
   pages     = {208--214}
}

@inproceedings{LNAI78980215,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Graeme Gange and Harald S{\o}ndergaard and Peter J. Stuckey and Peter Schachte},
   title     = {Solving Difference Constraints over Modular Arithmetic},
   pages     = {215--230}
}

@inproceedings{LNAI78980231,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Serdar Erbatur and Santiago Escobar and Deepak Kapur and Zhiqiang Liu and Christopher A. Lynch and Catherine Meadows and Jos\'{e} Meseguer and Paliath Narendran and Sonia Santiago and Ralf Sasse},
   title     = {Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis},
   pages     = {231--248}
}

@inproceedings{LNAI78980249,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Serdar Erbatur and Deepak Kapur and Andrew M. Marshall and Paliath Narendran and Christophe Ringeissen},
   title     = {Hierarchical Combination},
   pages     = {249--266}
}

@inproceedings{LNAI78980267,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Cezary Kaliszyk and Josef Urban},
   title     = {PRocH: Proof Reconstruction for {\sf HOL Light}},
   pages     = {267--274}
}

@inproceedings{LNAI78980275,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Rajeev Gor\'{e} and Jimmy Thomson},
   title     = {An Improved BDD Method for Intuitionistic Propositional Logic: <Literal>BDDIntKt</Literal> System Description},
   pages     = {275--281}
}

@inproceedings{LNAI78980282,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Chris Hawblitzel and Ming Kawaguchi and Shuvendu K. Lahiri and Henrique Reb\^{e}lo},
   title     = {Towards Modularly Comparing Programs Using Automated Theorem Provers},
   pages     = {282--299}
}

@inproceedings{LNAI78980300,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Reiner H\"{a}hnle and Ina Schaefer and Richard Bubel},
   title     = {Reuse in Software Verification by Abstract Method Calls},
   pages     = {300--314}
}

@inproceedings{LNAI78980315,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Bernhard Beckert and Daniel Bruns},
   title     = {Dynamic Logic with Trace Semantics},
   pages     = {315--329}
}

@inproceedings{LNAI78980330,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Franz Baader and Stefan Borgwardt and Marcel Lippmann},
   title     = {Temporalizing Ontology-Based Data Access},
   pages     = {330--344}
}

@inproceedings{LNAI78980345,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Marijn J.H. Heule and Warren A. Hunt Jr. and Nathan Wetzler},
   title     = {Verifying Refutations with Extended Resolution},
   pages     = {345--359}
}

@inproceedings{LNAI78980360,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Viorica Sofronie-Stokkermans},
   title     = {Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems},
   pages     = {360--376}
}

@inproceedings{LNAI78980377,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Andrew Reynolds and Cesare Tinelli and Amit Goel and Sava Krsti\'{c} and Morgan Deters and Clark Barrett},
   title     = {Quantifier Instantiation Techniques for Finite Model Finding in SMT},
   pages     = {377--391}
}

@inproceedings{LNAI78980392,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Koen Claessen and Moa Johansson and Dan Ros\'{e}n and Nicholas Smallbone},
   title     = {Automating Inductive Proofs Using Theory Exploration},
   pages     = {392--406}
}

@inproceedings{LNAI78980407,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Daniel K\"{u}hlwein and Stephan Schulz and Josef Urban},
   title     = {E-MaLeS 1.1},
   pages     = {407--413}
}

@inproceedings{LNAI78980414,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Jasmin Christian Blanchette and Andrei Paskevich},
   title     = {TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism},
   pages     = {414--420}
}

@inproceedings{LNAI78980421,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Richard Williams and Boris Konev},
   title     = {Propositional Temporal Proving with Reductions to a SAT Problem},
   pages     = {421--435}
}

@inproceedings{LNAI78980436,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Mark Kaminski and Tobias Tebbi},
   title     = {InKreSAT: Modal Reasoning via Incremental Reduction to SAT},
   pages     = {436--442}
}

@inproceedings{LNAI78980443,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Gergely Kov\'{a}sznai and Andreas Fr\"{o}hlich and Armin Biere},
   title     = {$\hbox{\sc bv2epr}$: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into $\hbox{\sc EPR}$},
   pages     = {443--449}
}

@inproceedings{LNAI78980450,
   editor    = {Maria Paola Bonacina},
   booktitle = {Automated Deduction -- CADE-24},
   publisher = {Springer},
   location  = {Heidelberg},
   series    = {Lecture Notes in Computer Science},
   volume    = {7898},
   year      = {2013},
   isbn      = {978-3-642-38573-5},
   author    = {Kry\v{s}tof Hoder and Andrei Voronkov},
   title     = {The 481 Ways to Split a Clause and Deal with Propositional Variables},
   pages     = {450--464}
}