| 2013 | A Graphical Language for Proof Strategies. Gudmund Grov, Aleks Kissinger, Yuhui Lin |
| 2013 | A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus. Tom Gundersen, Willem Heijltjes, Michel Parigot |
| 2013 | A Seligman-Style Tableau System. Patrick Blackburn, Thomas Bolander, Torben Braüner, Klaus Frovin Jørgensen |
| 2013 | A Semantic Basis for Proof Queries and Transformations. David Aspinall, Ewen Denney, Christoph Lüth |
| 2013 | An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics. Luca Aceto, Dario Della Monica, Anna Ingólfsdóttir, Angelo Montanari, Guido Sciavicco |
| 2013 | An Event Structure Model for Probabilistic Concurrent Kleene Algebra. Annabelle McIver, Tahiry M. Rabehaja, Georg Struth |
| 2013 | Blocked Clause Decomposition. Marijn Heule, Armin Biere |
| 2013 | Characterizing Subset Spaces as Bi-topological Structures. Bernhard Heinemann |
| 2013 | Comparison of LTL to Deterministic Rabin Automata Translators. Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek |
| 2013 | Complexity Analysis in Presence of Control Operators and Higher-Order Functions. Ugo Dal Lago, Giulio Pellitta |
| 2013 | Defining Privacy Is Supposed to Be Easy. Sebastian Mödersheim, Thomas Groß, Luca Viganò |
| 2013 | Description Logics, Rules and Multi-context Systems. Luís Cruz-Filipe, Rita Henriques, Isabel Nunes |
| 2013 | Dynamic and Static Symmetry Breaking in Answer Set Programming. Belaid Benhamou |
| 2013 | Expressive Path Queries on Graphs with Data. Pablo Barceló, Gaëlle Fontaine, Anthony Widjaja Lin |
| 2013 | Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies. Patrick Koopmann, Renate A. Schmidt |
| 2013 | Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. Syeda Hira Taqdees, Osman Hasan |
| 2013 | HOL Based First-Order Modal Logic Provers. Christoph Benzmüller, Thomas Raths |
| 2013 | Herbrand Theorems for Substructural Logics. Petr Cintula, George Metcalfe |
| 2013 | Incremental Tabling for Query-Driven Propagation of Logic Program Updates. Ari Saptawijaya, Luís Moniz Pereira |
| 2013 | Lemma Mining over HOL Light. Cezary Kaliszyk, Josef Urban |
| 2013 | Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov |
| 2013 | Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. Uwe Egly, Florian Lonsing, Magdalena Widl |
| 2013 | Maximal Falsifiability - Definitions, Algorithms, and Applications. Alexey Ignatiev, António Morgado, Jordi Planes, João Marques-Silva |
| 2013 | May-Happen-in-Parallel Analysis for Priority-Based Scheduling. Elvira Albert, Samir Genaim, Enrique Martin-Martin |
| 2013 | Multi-objective Discounted Reward Verification in Graphs and MDPs. Krishnendu Chatterjee, Vojtech Forejt, Dominik Wojtczak |
| 2013 | On Minimality and Integrity Constraints in Probabilistic Abduction. Calin-Rares Turliuc, Nataly Maimari, Alessandra Russo, Krysia Broda |
| 2013 | On Module-Based Abstraction and Repair of Behavioral Programs. Guy Katz |
| 2013 | On Promptness in Parity Games. Fabio Mogavero, Aniello Murano, Loredana Sorrentino |
| 2013 | On QBF Proofs and Preprocessing. Mikolás Janota, Radu Grigore, João Marques-Silva |
| 2013 | Partial Backtracking in CDCL Solvers. Chuan Jiang, Ting Zhang |
| 2013 | PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina |
| 2013 | Polar: A Framework for Proof Refactoring. Dominik Dietrich, Iain Whiteside, David Aspinall |
| 2013 | Polarizing Double-Negation Translations. Mélanie Boudard, Olivier Hermant |
| 2013 | Prediction and Explanation over DL-Lite Data Streams. Szymon Klarman, Thomas Meyer |
| 2013 | Proof-Pattern Recognition and Lemma Discovery in ACL2. Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, Ewen Maclean |
| 2013 | Proving Infinite Satisfiability. Peter Baumgartner, Joshua Bax |
| 2013 | Putting Newton into Practice: A Solver for Polynomial Equations over Semirings. Maximilian Schlund, Michal Terepeta, Michael Luttenberger |
| 2013 | Reachability Modules for the Description Logic $\mathcal{SRIQ}$. Riku Nortje, Katarina Britz, Thomas Meyer |
| 2013 | Relaxing Synchronization Constraints in Behavioral Programs. David Harel, Amir Kantor, Guy Katz |
| 2013 | Resourceful Reachability as HORN-LA. Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger |
| 2013 | Revisiting the Equivalence of Shininess and Politeness. Filipe Casal, João Rasga |
| 2013 | SAT-Based Preprocessing for MaxSAT. Anton Belov, António Morgado, João Marques-Silva |
| 2013 | Semantic A-translations and Super-Consistency Entail Classical Cut Elimination. Lisa Allali, Olivier Hermant |
| 2013 | Simulating Parity Reasoning. Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä |
| 2013 | Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |
| 2013 | System Description: E 1.8. Stephan Schulz |
| 2013 | The Complexity of Clausal Fragments of LTL. Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev |
| 2013 | Three SCC-Based Emptiness Checks for Generalized Büchi Automata. Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2013 | Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic. Giovanni Casini, Umberto Straccia |
| 2013 | Tracking Data-Flow with Open Closure Types. Gabriel Scherer, Jan Hoffmann |
| 2013 | Tree Interpolation in Vampire. Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl |
| 2013 | Verifying Temporal Properties in Real Models. Tim French, John Christopher McCabe-Dansted, Mark Reynolds |
| 2013 | Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant |