Abstract is missing.
- Programming by Composing FiltersJeffrey Fischer, Rupak Majumdar. 1-13 [doi]
- Theorem Provers For Every Normal Modal LogicTobias Gleißner, Alexander Steen, Christoph Benzmüller. 14-30 [doi]
- Blocked Clauses in First-Order LogicBenjamin Kiesl, Martin Suda 0001, Martina Seidl, Hans Tompits, Armin Biere. 31-48 [doi]
- First-Order Interpolation and Interpolating Proof SystemsLaura Kovács, Andrei Voronkov. 49-64 [doi]
- Towards a Semantics of Unsatisfiability Proofs with InprocessingTobias Philipp, Adrián Rebola-Pardo. 65-84 [doi]
- Deep Network Guided Proof SearchSarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk. 85-105 [doi]
- Deep Proof Search in MELLOzan Kahramanogullari. 106-124 [doi]
- TacticToe: Learning to Reason with HOL4 TacticsThibault Gauthier, Cezary Kaliszyk, Josef Urban. 125-143 [doi]
- Automated analysis of Stateflow modelsHamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux. 144-161 [doi]
- Quantified Boolean Formulas: Call the Plumber!Josef Lindsberger, Alexander Maringele, Georg Moser. 162-170 [doi]
- Cauliflower: a Solver Generator for Context-Free Language ReachabilityNicholas Hollingum, Bernhard Scholz. 171-180 [doi]
- Decidable linear list constraintsSabine Bauer, Martin Hofmann. 181-199 [doi]
- RACCOON: A Connection Reasoner for the Description Logic ALCDimas Melo Filho, Fred Freitas, Jens Otten. 200-211 [doi]
- On the Interaction of Inclusion Dependencies with Independence AtomsMiika Hannula, Juha Kontinen, Sebastian Link. 212-226 [doi]
- Propagators and Solvers for the Algebra of Modular SystemsBart Bogaerts 0001, Eugenia Ternovska, David G. Mitchell. 227-248 [doi]
- Analyzing Runtime Complexity via Innermost Runtime ComplexityFlorian Frohn, Jürgen Giesl. 249-268 [doi]
- Higher order interpretation for higher order complexityEmmanuel Hainry, Romain Péchoux. 269-285 [doi]
- From SAT to Maximum Independent Set: A New Approach to Characterize Tractable ClassesYazid Boumarafi, Lakhdar Sais, Yakoub Salhi. 286-299 [doi]
- Parallel Graph Rewriting with Overlapping RulesRachid Echahed, Aude Maignan. 300-318 [doi]
- A Quantitative Partial Model-Checking Function and Its OptimisationStefano Bistarelli, Fabio Martinelli, Ilaria Matteucci, Francesco Santini. 319-337 [doi]
- Synchronizing Constrained Horn ClausesDmitry Mordvinov, Grigory Fedyukovich. 338-355 [doi]
- Seminator: A Tool for Semi-Determinization of Omega-AutomataFrantisek Blahoudek, Alexandre Duret-Lutz, Mikulás Klokocka, Mojmír Kretínský, Jan Strejcek. 356-367 [doi]
- Quantified Heap Invariants for Object-Oriented ProgramsTemesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf. 368-384 [doi]
- Proving uniformity and independence by self-composition and couplingGilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. 385-403 [doi]
- Gödel logics and the fully boxed fragment of LTLMatthias Baaz, Norbert Preining. 404-416 [doi]
- Bunched Hypersequent Calculi for Distributive Substructural LogicsAgata Ciabattoni, Revantha Ramanayake. 417-434 [doi]
- A uniform framework for substructural logics with modalitiesBjörn Lellmann, Carlos Olarte, Elaine Pimentel. 435-455 [doi]
- A One-Pass Tree-Shaped Tableau for LTL+PastNicola Gigante, Angelo Montanari, Mark Reynolds. 456-473 [doi]
- Coq without Type Casts: A Complete Proof of Coq Modulo TheoryJean-Pierre Jouannaud, Pierre-Yves Strub. 474-489 [doi]
- Reasoning about Translation Lookaside BuffersHira Syeda, Gerwin Klein. 490-508 [doi]
- Formally Proving the Boolean Pythagorean Triples ConjectureLuís Cruz-Filipe, Peter Schneider-Kamp. 509-522 [doi]