| 2010 | A Decidable Class of Nested Iterated Schemata. Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2010 | A Decision Procedure for CTL Oliver Friedmann, Markus Latte, Martin Lange |
| 2010 | A Single-Significant-Digit Calculus for Semi-Automated Guesstimation. Jonathan Alexander Abourbih, Luke Blaney, Alan Bundy, Fiona McNeill |
| 2010 | A Slice-Based Decision Procedure for Type-Based Partial Orders. Elena Sherman, Brady J. Garvin, Matthew B. Dwyer |
| 2010 | An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ. Yevgeny Kazakov |
| 2010 | An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
| 2010 | Analytic Tableaux for Higher-Order Logic with Choice. Julian Backes, Chad E. Brown |
| 2010 | Automated Reasoning for Relational Probabilistic Knowledge Representation. Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner, Matthias Thimm |
| 2010 | Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings Jürgen Giesl, Reiner Hähnle |
| 2010 | Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion. Markus Aderhold |
| 2010 | Automating Security Analysis: Symbolic Equivalence of Constraint Systems. Vincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune |
| 2010 | Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). Brigitte Pientka, Jana Dunfield |
| 2010 | Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. Leonardo Mendonça de Moura, Nikolaj S. Bjørner |
| 2010 | Classical Logic with Partial Functions. Hans de Nivelle |
| 2010 | Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus. Anders Schack-Nielsen, Carsten Schürmann |
| 2010 | Decreasing Diagrams and Relative Termination. Nao Hirokawa, Aart Middeldorp |
| 2010 | Focused Inductive Theorem Proving. David Baelde, Dale Miller, Zachary Snow |
| 2010 | Global Caching for Coalgebraic Description Logics. Rajeev Goré, Clemens Kupke, Dirk Pattinson, Lutz Schröder |
| 2010 | Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic. Marta Cialdea Mayer, Serenella Cerrito |
| 2010 | Hierarchical Reasoning for the Verification of Parametric Systems. Viorica Sofronie-Stokkermans |
| 2010 | Induction, Invariants, and Abstraction. Deepak Kapur |
| 2010 | Interpolation and Symbol Elimination in Vampire. Krystof Hoder, Laura Kovács, Andrei Voronkov |
| 2010 | Linear Quantifier Elimination as an Abstract Decision Procedure. Nikolaj S. Bjørner |
| 2010 | Logic between Expressivity and Complexity. Johan van Benthem |
| 2010 | MCMT: A Model Checker Modulo Theories. Silvio Ghilardi, Silvio Ranise |
| 2010 | MUNCH - Automated Reasoner for Sets and Multisets. Ruzica Piskac, Viktor Kuncak |
| 2010 | Monotonicity Criteria for Polynomial Interpretations over the Naturals. Friedrich Neurauter, Aart Middeldorp, Harald Zankl |
| 2010 | Monotonicity Inference for Higher-Order Formulas. Jasmin Christian Blanchette, Alexander Krauss |
| 2010 | Multi-Prover Verification of Floating-Point Programs. Ali Ayad, Claude Marché |
| 2010 | On Hierarchical Reasoning in Combinations of Theories. Carsten Ihlemann, Viorica Sofronie-Stokkermans |
| 2010 | On the Saturation of YAGO. Martin Suda, Christoph Weidenbach, Patrick Wischnewski |
| 2010 | Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse. Rajeev Goré, Florian Widmann |
| 2010 | Optimized Description Logic Reasoning via Core Blocking. Birte Glimm, Ian Horrocks, Boris Motik |
| 2010 | Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2010 | Premise Selection in the Naproche System. Marcos Cramer, Peter Koepke, Daniel Kühlwein, Bernhard Schröder |
| 2010 | RegSTAB: A SAT Solver for Propositional Schemata. Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier |
| 2010 | Sledgehammer: Judgement Day. Sascha Böhme, Tobias Nipkow |
| 2010 | System Description: The Proof Transformation System CERES. Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo |
| 2010 | Terminating Tableaux for Hybrid Logic with Eventualities. Mark Kaminski, Gert Smolka |
| 2010 | Termination Tools in Ordered Completion. Sarah Winkler, Aart Middeldorp |
| 2010 | Tractable Extensions of the Description Logic Despoina Magka, Yevgeny Kazakov, Ian Horrocks |
| 2010 | URBiVA: Uniform Reduction to Bit-Vector Arithmetic. Filip Maric, Predrag Janicic |
| 2010 | Verifying Safety Properties with the TLA+ Proof System. Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2010 | iProver-Eq: An Instantiation-Based Theorem Prover with Equality. Konstantin Korovin, Christoph Sticksel |