PAAR-2016 Fifth Workshop on Practical Aspects of Automated Reasoning July 2, 2016 Affiliated with the 8th International Joint Conference on Automated Reasoning (IJCAR 2016) Coimbra, Portugal http://cs.ru.nl/paar16/ Preface This volume contains the papers presented at the Fifth Workshop on Practical Aspects of Automated Reasoning (PAAR-2016). The workshop was held on July 2, 2016, in Coimbra, Portugal, in association with the Eighth International Joint Conference on Automated Reasoning (IJCAR-2016). PAAR provides a forum for developers of automated reasoning tools to discuss and compare different im- plementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brings together different groups to concentrate on practical aspects of the implementation and appli- cation of automated reasoning tools. It allows researchers to present work in progress, and to discuss current trends, new implementation techniques and new applications. Papers were solicited on topics that include all practical aspects of automated reasoning. More specifically, some suggested topics were: • automated reasoning in propositional, first-order, higher-order and non-classical logics; • implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frame- works, etc); • automated reasoning tools for all kinds of practical problems and applications; • pragmatics of automated reasoning within proof assistants; • practical experiences, usability aspects, feasibility studies; • evaluation of implementation techniques and automated reasoning tools; • performance aspects, benchmarking approaches; • non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new appli- cations; • implementation techniques, optimization techniques, strategies and heuristics, fairness; • support tools for prover development; • system descriptions and demos. PAAR is particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems in practice, and how to apply existing systems to real problems. The workshop received thirteen submissions. Each submission was reviewed by at least three program com- mittee members, and eleven papers were accepted for presentation at the workshop and inclusion into the pro- ceedings. The papers cover a broad area, with topics ranging from improved techniques for SMT and first-order reasoning to proof reconstruction, application of reasoners to modal logic, and logic language design. The workshop organizers would like to thank the authors and participants of the workshop for helping making this a successful event. Our particular thanks go the program committee and the external reviewers for their considerable effort to provide very good reviews, often even in time. We are also grateful to the IJCAR organizers for their support and for hosting the workshop, and are indebted to the EasyChair team for the availability of the EasyChair Conference System. June 2016 Pascal Fontaine, Stephan Schulz, Josef Urban II Program Committee June Andronick (NICTA and University of New South Wales, Australia) Peter Baumgartner (NICTA/Australian National University, Australia) Christoph Benzmüller (Freie Universität Berlin, Germany) Armin Bierre (Johannes Kepler University, Austria) Nikolaj Bjorner (Microsoft Research, USA) Simon Cruanes (Loria, INRIA, France) Hans de Nivelle (University of Wroclaw, Poland) Pascal Fontaine (Loria, INRIA, University of Lorraine, France), co-chair Vijay Ganesh (University of Waterloo, Canada) Alberto Griggio (FBK-IRST, Italy) John Harrison (Intel, USA) Marijn Heule (The University of Texas at Austin, USA) Dejan Jovanović (SRI International, USA) Yevgeny Kazakov (The University of Ulm, Germany) Chantal Keller (LRI, Université Paris-Sud, France) Boris Konev (The University of Liverpool, UK) Konstantin Korovin (The University of Manchester, UK) Laura Kovacs (Chalmers University, Sweden) Jens Otten (University of Potsdam, Germany) Nicolas Peltier (CNRS - LIG, France) Ruzica Piskac (Yale University, USA) Giles Reger (The University of Manchester, UK) Andrew Reynolds (EPFL, Switzerland) Philipp Ruemmer (Uppsala University, Sweden) Uli Sattler (The University of Manchester, UK) Renate A. Schmidt (The University of Manchester, UK) Stephan Schulz (DHBW Stuttgart, Germany), co-chair Geoff Sutcliffe (University of Miami, USA) Josef Urban (Czech Technical University in Prague, Czech Republic), co-chair Uwe Waldmann (MPI Saarbrücken, Germany) External reviewers Peter Backeman Murphy Berzish Chad Brown Yizheng Zhao III Table of Contents Efficient Instantiation Techniques in SMT (Work In Progress) . . . . . . . . . . . . . . . . . . . . . . . . . 1 Haniel Barbosa Alternative treatments of common binary relations in first-order automated reasoning . . . . . . . . . . . 11 Koen Claessen and Ann Lillieström No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions . . . . . . . . . . . . . . 24 Michael Färber and Cezary Kaliszyk Deduction as a Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Mohamed Hassona and Stephan Schulz TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism . . . . . . . . . . . . . . . . . . . 41 Cezary Kaliszyk, Geoff Sutcliffe and Florian Rabe Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub . . . . . . . . . . . . . 56 Eugen Kuksa and Till Mossakowski On Checking Kripke Models for Modal Logic K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers . . . . . . . . . . 82 Tomer Libal and Alexander Steen Ordered Resolution with Straight Dismatching Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Andreas Teucke and Christoph Weidenbach A Saturation-based Algebraic Reasoner for ELQ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 Jelena Vlasenko, Maryam Daryalal, Volker Haarslev and Brigitte Jaumard The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating . . . . . . . . . . . . 125 Christoph Wernhard IV