Abstract is missing.
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda CalculusAnders Schack-Nielsen, Carsten Schürmann. 1-14 [doi]
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)Brigitte Pientka, Joshua Dunfield. 15-21 [doi]
- MCMT: A Model Checker Modulo TheoriesSilvio Ghilardi, Silvio Ranise. 22-29 [doi]
- On Hierarchical Reasoning in Combinations of TheoriesCarsten Ihlemann, Viorica Sofronie-Stokkermans. 30-45 [doi]
- Global Caching for Coalgebraic Description LogicsRajeev Goré, Clemens Kupke, Dirk Pattinson, Lutz Schröder. 46-60 [doi]
- Tractable Extensions of the Description Logic ::::EL:::: with Numerical DatatypesDespoina Magka, Yevgeny Kazakov, Ian Horrocks. 61-75 [doi]
- Analytic Tableaux for Higher-Order Logic with ChoiceJulian Backes, Chad E. Brown. 76-90 [doi]
- Monotonicity Inference for Higher-Order FormulasJasmin Christian Blanchette, Alexander Krauss. 91-106 [doi]
- Sledgehammer: Judgement DaySascha Böhme, Tobias Nipkow. 107-121 [doi]
- Logic between Expressivity and ComplexityJohan van Benthem. 122-126 [doi]
- Multi-Prover Verification of Floating-Point ProgramsAli Ayad, Claude Marché. 127-141 [doi]
- Verifying Safety Properties with the TLA+ Proof SystemKaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. 142-148 [doi]
- MUNCH - Automated Reasoner for Sets and MultisetsRuzica Piskac, Viktor Kuncak. 149-155 [doi]
- A Slice-Based Decision Procedure for Type-Based Partial OrdersElena Sherman, Brady J. Garvin, Matthew B. Dwyer. 156-170 [doi]
- Hierarchical Reasoning for the Verification of Parametric SystemsViorica Sofronie-Stokkermans. 171-187 [doi]
- Interpolation and Symbol Elimination in VampireKrystof Hoder, Laura Kovács, Andrei Voronkov. 188-195 [doi]
- iProver-Eq: An Instantiation-Based Theorem Prover with EqualityKonstantin Korovin, Christoph Sticksel. 196-202 [doi]
- Classical Logic with Partial FunctionsHans de Nivelle. 203-217 [doi]
- Automated Reasoning for Relational Probabilistic Knowledge RepresentationChristoph Beierle, Marc Finthammer, Gabriele Kern-Isberner, Matthias Thimm. 218-224 [doi]
- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with ConverseRajeev Goré, Florian Widmann. 225-239 [doi]
- Terminating Tableaux for Hybrid Logic with EventualitiesMark Kaminski, Gert Smolka. 240-254 [doi]
- Herod and Pilate: Two Tableau Provers for Basic Hybrid LogicMarta Cialdea Mayer, Serenella Cerrito. 255-262 [doi]
- Automated Synthesis of Induction Axioms for Programs with Second-Order RecursionMarkus Aderhold. 263-277 [doi]
- Focused Inductive Theorem ProvingDavid Baelde, Dale Miller, Zachary Snow. 278-292 [doi]
- A Decidable Class of Nested Iterated SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. 293-308 [doi]
- RegSTAB: A SAT Solver for Propositional SchemataVincent Aravantinos, Ricardo Caferra, Nicolas Peltier. 309-315 [doi]
- Linear Quantifier Elimination as an Abstract Decision ProcedureNikolaj Bjørner. 316-330 [doi]
- A Decision Procedure for CTL:::*::: Based on Tableaux and AutomataOliver Friedmann, Markus Latte, Martin Lange. 331-345 [doi]
- URBiVA: Uniform Reduction to Bit-Vector ArithmeticFilip Maric, Predrag Janicic. 346-352 [doi]
- Induction, Invariants, and AbstractionDeepak Kapur. 353 [doi]
- A Single-Significant-Digit Calculus for Semi-Automated GuesstimationJonathan A. Abourbih, Luke Blaney, Alan Bundy, Fiona McNeill. 354-368 [doi]
- Perfect Discrimination Graphs: Indexing Terms with Integer ExponentsHicham Bensaid, Ricardo Caferra, Nicolas Peltier. 369-383 [doi]
- An Interpolating Sequent Calculus for Quantifier-Free Presburger ArithmeticAngelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl. 384-399 [doi]
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software DevelopmentLeonardo Mendonça de Moura, Nikolaj Bjørner. 400-411 [doi]
- Automating Security Analysis: Symbolic Equivalence of Constraint SystemsVincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune. 412-426 [doi]
- System Description: The Proof Transformation System CERESTsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo. 427-433 [doi]
- Premise Selection in the Naproche SystemMarcos Cramer, Peter Koepke, Daniel Kühlwein, Bernhard Schröder. 434-440 [doi]
- On the Saturation of YAGOMartin Suda, Christoph Weidenbach, Patrick Wischnewski. 441-456 [doi]
- Optimized Description Logic Reasoning via Core BlockingBirte Glimm, Ian Horrocks, Boris Motik. 457-471 [doi]
- An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQYevgeny Kazakov. 472-486 [doi]
- Decreasing Diagrams and Relative TerminationNao Hirokawa, Aart Middeldorp. 487-501 [doi]
- Monotonicity Criteria for Polynomial Interpretations over the NaturalsFriedrich Neurauter, Aart Middeldorp, Harald Zankl. 502-517 [doi]
- Termination Tools in Ordered CompletionSarah Winkler, Aart Middeldorp. 518-532 [doi]