| 2013 | : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. Gergely Kovásznai, Andreas Fröhlich, Armin Biere |
| 2013 | A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies. Marta Cialdea Mayer |
| 2013 | A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker |
| 2013 | An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description. Rajeev Goré, Jimmy Thomson |
| 2013 | Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme. Bernhard Beckert, Rajeev Goré, Carsten Schürmann |
| 2013 | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2013 | Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings Maria Paola Bonacina |
| 2013 | Automated Reasoning, Fast and Slow. Natarajan Shankar |
| 2013 | Automating Inductive Proofs Using Theory Exploration. Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone |
| 2013 | Completeness and Decidability Results for First-Order Clauses with Indices. Abdelkader Kersani, Nicolas Peltier |
| 2013 | Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. Leonardo Mendonça de Moura, Grant Olney Passmore |
| 2013 | Computing Tiny Clause Normal Forms. Noran Azmy, Christoph Weidenbach |
| 2013 | Dynamic Logic with Trace Semantics. Bernhard Beckert, Daniel Bruns |
| 2013 | E-MaLeS 1.1. Daniel Kühlwein, Stephan Schulz, Josef Urban |
| 2013 | Foundational Proof Certificates in First-Order Logic. Zakaria Chihani, Dale Miller, Fabien Renaud |
| 2013 | Hierarchic Superposition with Weak Abstraction. Peter Baumgartner, Uwe Waldmann |
| 2013 | Hierarchical Combination. Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen |
| 2013 | Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems. Viorica Sofronie-Stokkermans |
| 2013 | InKreSAT: Modal Reasoning via Incremental Reduction to SAT. Mark Kaminski, Tobias Tebbi |
| 2013 | One Logic to Use Them All. Jean-Christophe Filliâtre |
| 2013 | PRocH: Proof Reconstruction for HOL Light. Cezary Kaliszyk, Josef Urban |
| 2013 | Propositional Temporal Proving with Reductions to a SAT Problem. Richard Williams, Boris Konev |
| 2013 | Quantifier Instantiation Techniques for Finite Model Finding in SMT. Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
| 2013 | Reuse in Software Verification by Abstract Method Calls. Reiner Hähnle, Ina Schaefer, Richard Bubel |
| 2013 | Solving Difference Constraints over Modular Arithmetic. Graeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte |
| 2013 | System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description Logic. Markus Bender, Björn Pelzer, Claudia Schon |
| 2013 | TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. Jasmin Christian Blanchette, Andrei Paskevich |
| 2013 | Temporalizing Ontology-Based Data Access. Franz Baader, Stefan Borgwardt, Marcel Lippmann |
| 2013 | The 481 Ways to Split a Clause and Deal with Propositional Variables. Krystof Hoder, Andrei Voronkov |
| 2013 | The Tree Width of Separation Logic with Recursive Definitions. Radu Iosif, Adam Rogalewicz, Jirí Simácek |
| 2013 | Towards Modularly Comparing Programs Using Automated Theorem Provers. Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo |
| 2013 | Tractable Inference Systems: An Extension with a Deducibility Predicate. Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri |
| 2013 | Verifying Refutations with Extended Resolution. Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | dReal: An SMT Solver for Nonlinear Theories over the Reals. Sicun Gao, Soonho Kong, Edmund M. Clarke |