| 2012 | A Calculus for Generating Ground Explanations. Mnacho Echenim, Nicolas Peltier |
| 2012 | A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. Martin Suda, Christoph Weidenbach |
| 2012 | A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
| 2012 | Automated Analysis of Regular Algebra. Simon Foster, Georg Struth |
| 2012 | Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings Bernhard Gramlich, Dale Miller, Uli Sattler |
| 2012 | Automated Verification of Recursive Programs with Pointers. Frank S. de Boer, Marcello M. Bonsangue, Jurriaan Rot |
| 2012 | BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics. Rajeev Goré, Jimmy Thomson |
| 2012 | Branching Time? Pruning Time! Markus Latte, Martin Lange |
| 2012 | Combination of Disjoint Theories: Beyond Decidability. Pascal Fontaine, Stephan Merz, Christoph Weidenbach |
| 2012 | Correctness of Program Transformations as a Termination Problem. Conrad Rau, David Sabel, Manfred Schmidt-Schauß |
| 2012 | Diabelli: A Heterogeneous Proof System. Matej Urbas, Mateja Jamnik |
| 2012 | EPR-Based Bounded Model Checking at Word Level. Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov |
| 2012 | Effective Finite-Valued Semantics for Labelled Calculi. Matthias Baaz, Ori Lahav, Anna Zamansky |
| 2012 | Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics. Yuri V. Matiyasevich |
| 2012 | Extended Caching, Backjumping and Merging for Expressive Description Logics. Andreas Steigmiller, Thorsten Liebig, Birte Glimm |
| 2012 | Fingerprint Indexing for Paramodulation and Rewriting. Stephan Schulz |
| 2012 | From Linear Temporal Logic Properties to Rewrite Propositions. Pierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko |
| 2012 | From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise |
| 2012 | How Fuzzy Is My Fuzzy Description Logic? Stefan Borgwardt, Felix Distel, Rafael Peñaloza |
| 2012 | Inprocessing Rules. Matti Järvisalo, Marijn Heule, Armin Biere |
| 2012 | KBCV - Knuth-Bendix Completion Visualizer. Thomas Sternagel, Harald Zankl |
| 2012 | Logical Difference Computation with CEX2.5. Boris Konev, Michel Ludwig, Frank Wolter |
| 2012 | New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants. Andrew M. Marshall, Paliath Narendran |
| 2012 | Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. Roberto Sebastiani, Silvia Tomasi |
| 2012 | Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes |
| 2012 | Playing Hybrid Games with KeYmaera. Jan-David Quesel, André Platzer |
| 2012 | Proving Non-looping Non-termination Automatically. Fabian Emmes, Tim Enger, Jürgen Giesl |
| 2012 | Reachability Analysis of Program Variables. Durica Nikolic, Fausto Spoto |
| 2012 | Rewriting Induction + Linear Arithmetic = Decision Procedure. Stephan Falke, Deepak Kapur |
| 2012 | SAT Encoding of Unification in ℇℒℋ Franz Baader, Stefan Borgwardt, Barbara Morawska |
| 2012 | SAT and SMT Are Still Resolution: Questions and Challenges. Robert Nieuwenhuis |
| 2012 | SPARQL Query Containment under RDFS Entailment Regime. Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès, Nabil Layaïda |
| 2012 | Satallax: An Automatic Higher-Order Prover. Chad E. Brown |
| 2012 | Security Protocols, Constraint Systems, and Group Theories. Stéphanie Delaune, Steve Kremer, Daniel Pasaila |
| 2012 | Solving Non-linear Arithmetic. Dejan Jovanovic, Leonardo Mendonça de Moura |
| 2012 | Stratification in Logics of Definitions. Alwen Tiu |
| 2012 | Synthesis for Unbounded Bit-Vector Arithmetic. Andrej Spielmann, Viktor Kuncak |
| 2012 | Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
| 2012 | Taking Satisfiability to the Next Level with Z3 - (Abstract). Nikolaj S. Bjørner |
| 2012 | Taming Past LTL and Flat Counter Systems. Stéphane Demri, Amit Kumar Dhar, Arnaud Sangnier |
| 2012 | The QMLTP Problem Library for First-Order Modal Logics. Thomas Raths, Jens Otten |
| 2012 | Truthful Monadic Abstractions. Taus Brock-Nannestad, Carsten Schürmann |
| 2012 | UEL: Unification Solver for the Description Logic ℇℒ - System Description. Franz Baader, Julian Mendez, Barbara Morawska |
| 2012 | Unification Modulo Synchronous Distributivity. Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch |
| 2012 | δ-Complete Decision Procedures for Satisfiability over the Reals. Sicun Gao, Jeremy Avigad, Edmund M. Clarke |