Automated Reasoning

Logical Frameworks and Combination of Systems.- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus.- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description).- MCMT: A Model Checker Modulo Theories.- On Hierarchical Reasoning in Combinations of Theories.- Description Logic I.- Global Caching for Coalgebraic Description Logics.- Tractable Extensions of the Description Logic with Numerical Datatypes.- Higher-Order Logic.- Analytic Tableaux for Higher-Order Logic with Choice.- Monotonicity Inference for Higher-Order Formulas.- Sledgehammer: Judgement Day.- Invited Talk.- Logic between Expressivity and Complexity.- Verification.- Multi-Prover Verification of Floating-Point Programs.- Verifying Safety Properties with the TLA?+? Proof System.- MUNCH - Automated Reasoner for Sets and Multisets.- A Slice-Based Decision Procedure for Type-Based Partial Orders.- Hierarchical Reasoning for the Verification of Parametric Systems.- First-Order Logic.- Interpolation and Symbol Elimination in Vampire.- iProver-Eq: An Instantiation-Based Theorem Prover with Equality.- Classical Logic with Partial Functions.- Non-Classical Logic.- Automated Reasoning for Relational Probabilistic Knowledge Representation.- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse.- Terminating Tableaux for Hybrid Logic with Eventualities.- Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic.- Induction.- Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion.- Focused Inductive Theorem Proving.- Decision Procedures.- A Decidable Class of Nested Iterated Schemata.- RegSTAB: A SAT Solver for Propositional Schemata.- Linear Quantifier Elimination as an Abstract Decision Procedure.- A Decision Procedure for CTL* Based on Tableaux and Automata.- URBiVA: Uniform Reduction to Bit-Vector Arithmetic.- Keynote Talk.- Induction, Invariants, and Abstraction.- Arithmetic.- A