Abstract is missing.
- One Logic to Use Them AllJean-Christophe Filliâtre. 1-20 [doi]
- The Tree Width of Separation Logic with Recursive DefinitionsRadu Iosif, Adam Rogalewicz, Jirí Simácek. 21-38 [doi]
- Hierarchic Superposition with Weak AbstractionPeter Baumgartner, Uwe Waldmann. 39-57 [doi]
- Completeness and Decidability Results for First-Order Clauses with IndicesAbdelkader Kersani, Nicolas Peltier. 58-75 [doi]
- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation HierarchiesMarta Cialdea Mayer. 76-90 [doi]
- Tractable Inference Systems: An Extension with a Deducibility PredicateHubert Comon-Lundh, Véronique Cortier, Guillaume Scerri. 91-108 [doi]
- Computing Tiny Clause Normal FormsNoran Azmy, Christoph Weidenbach. 109-125 [doi]
- System Description: E-KRHyper 1.4 - Extensions for Unique Names and Description LogicMarkus Bender, Björn Pelzer, Claudia Schon. 126-134 [doi]
- Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election SchemeBernhard Beckert, Rajeev Goré, Carsten Schürmann. 135-144 [doi]
- Automated Reasoning, Fast and SlowNatarajan Shankar. 145-161 [doi]
- Foundational Proof Certificates in First-Order LogicZakaria Chihani, Dale Miller, Fabien Renaud. 162-177 [doi]
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the RationalsLeonardo Mendonça de Moura, Grant Olney Passmore. 178-192 [doi]
- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic DecompositionUlrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker. 193-207 [doi]
- dReal: An SMT Solver for Nonlinear Theories over the RealsSicun Gao, Soonho Kong, Edmund M. Clarke. 208-214 [doi]
- Solving Difference Constraints over Modular ArithmeticGraeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte. 215-230 [doi]
- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol AnalysisSerdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse. 231-248 [doi]
- Hierarchical CombinationSerdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen. 249-266 [doi]
- PRocH: Proof Reconstruction for HOL LightCezary Kaliszyk, Josef Urban. 267-274 [doi]
- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System DescriptionRajeev Goré, Jimmy Thomson. 275-281 [doi]
- Towards Modularly Comparing Programs Using Automated Theorem ProversChris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo. 282-299 [doi]
- Reuse in Software Verification by Abstract Method CallsReiner Hähnle, Ina Schaefer, Richard Bubel. 300-314 [doi]
- Dynamic Logic with Trace SemanticsBernhard Beckert, Daniel Bruns. 315-329 [doi]
- Temporalizing Ontology-Based Data AccessFranz Baader, Stefan Borgwardt, Marcel Lippmann. 330-344 [doi]
- Verifying Refutations with Extended ResolutionMarijn Heule, Warren A. Hunt Jr., Nathan Wetzler. 345-359 [doi]
- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid SystemsViorica Sofronie-Stokkermans. 360-376 [doi]
- Quantifier Instantiation Techniques for Finite Model Finding in SMTAndrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett. 377-391 [doi]
- Automating Inductive Proofs Using Theory ExplorationKoen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone. 392-406 [doi]
- E-MaLeS 1.1Daniel Kühlwein, Stephan Schulz, Josef Urban. 407-413 [doi]
- TFF1: The TPTP Typed First-Order Form with Rank-1 PolymorphismJasmin Christian Blanchette, Andrei Paskevich. 414-420 [doi]
- Propositional Temporal Proving with Reductions to a SAT ProblemRichard Williams, Boris Konev. 421-435 [doi]
- InKreSAT: Modal Reasoning via Incremental Reduction to SATMark Kaminski, Tobias Tebbi. 436-442 [doi]
- : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas intoGergely Kovásznai, Andreas Fröhlich, Armin Biere. 443-449 [doi]
- The 481 Ways to Split a Clause and Deal with Propositional VariablesKrystof Hoder, Andrei Voronkov. 450-464 [doi]