| 2013 | Partial Backtracking in CDCL Solvers. | Chuan Jiang, Ting Zhang |
| 2013 | On QBF Proofs and Preprocessing. | Mikols Janota, Radu Grigore, Joo Marques-Silva |
| 2013 | Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. | Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |
| 2013 | Maximal Falsifiability - Definitions, Algorithms, and Applications. | Alexey Ignatiev, Antnio Morgado, Jordi Planes, Joo Marques-Silva |
| 2013 | Blocked Clause Decomposition. | Marijn Heule, Armin Biere |
| 2013 | Proof-Pattern Recognition and Lemma Discovery in ACL2. | Jnathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean |
| 2013 | Characterizing Subset Spaces as Bi-topological Structures. | Bernhard Heinemann |
| 2013 | Relaxing Synchronization Constraints in Behavioral Programs. | David Harel, Amir Kantor, Guy Katz |
| 2013 | A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus. | Tom Gundersen, Willem Heijltjes, Michel Parigot |
| 2013 | A Graphical Language for Proof Strategies. | Gudmund Grov, Aleks Kissinger, Yuhui Lin |
| 2013 | Verifying Temporal Properties in Real Models. | Tim French, John Christopher McCabe-Dansted, Mark Reynolds |
| 2013 | Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. | Uwe Egly, Florian Lonsing, Magdalena Widl |
| 2013 | Robotics, Temporal Logic and Stream Reasoning. | Patrick Doherty, Fredrik Heintz, Jonas Kvarnstrm |
| 2013 | Polar: A Framework for Proof Refactoring. | Dominik Dietrich, Iain Whiteside, David Aspinall |
| 2013 | Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. | David Delahaye, Damien Doligez, Frdric Gilbert, Pierre Halmagrand, Olivier Hermant |
| 2013 | Description Logics, Rules and Multi-context Systems. | Lus Cruz-Filipe, Rita Henriques, Isabel Nunes |
| 2013 | Herbrand Theorems for Substructural Logics. | Petr Cintula, George Metcalfe |
| 2013 | Multi-objective Discounted Reward Verification in Graphs and MDPs. | Krishnendu Chatterjee, Vojtech Forejt, Dominik Wojtczak |
| 2013 | Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gdel Logic. | Giovanni Casini, Umberto Straccia |
| 2013 | Revisiting the Equivalence of Shininess and Politeness. | Filipe Casal, Joo Rasga |
| 2013 | Polarizing Double-Negation Translations. | Mlanie Boudard, Olivier Hermant |
| 2013 | Tree Interpolation in Vampire. | Rgis Blanc, Ashutosh Gupta, Laura Kovcs, Bernhard Kragl |
| 2013 | Comparison of LTL to Deterministic Rabin Automata Translators. | Frantisek Blahoudek, Mojmr Kretnsk, Jan Strejcek |
| 2013 | A Seligman-Style Tableau System. | Patrick Blackburn, Thomas Bolander, Torben Braner, Klaus Frovin Jrgensen |
| 2013 | Instantiations, Zippers and EPR Interpolation. | Nikolaj S. Bjrner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav |