This volume contains the papers presented at the Workshop on Practical Aspects of Automated Reasoning (PAAR-2018). The workshop was held on July 19, 2018, in Oxford, UK, in association with the Federated Logic Conference 2018. This is the sixth, tenth year anniversary, edition of the workshop. The workshop series started in 2008 with the first workshop in Sydney, Australia, followed by Edinburgh, UK (2010), Manchester, UK (2012), Vienna, Austria (2014) and Coimbra, Portugal (2016).
PAAR provided a forum for developers of automated reasoning tools to discuss and compare di↵erent implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brought together di↵erent groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It allowed researchers to present their work in progress, and to discuss new implementation techniques and applications.
Papers were solicited on topics that include all practical aspects of automated reasoning, including but not limited to – automated reasoning in propositional, first-order, higher-order, and nonclassical logics; – implementation of provers (SAT, SMT, resolution, tableau, instantiationbased, rewriting, logical frameworks, etc.); – automated reasoning tools for all kinds of practical problems and applications; – pragmatics of automated reasoning with 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 applications; – implementation techniques, optimisation techniques, strategies and heuristics, fairness; – tools or methods that support prover development; – system descriptions and demos.
The workshop received seven submissions. Each submission was reviewed by at least three members of the program committee. The committee decided to accept all seven papers for presentation at the workshop and for inclusion into the proceedings. The program also includes an invited talk. The papers cover a wide area of topics ranging from the use of machine learning to guide proof search to higher-order reasoning and specification languages to proof methods and verified tools.
The workshop organizers would like to thank the authors and participants of the workshop for helping to make this a successful event. Our particular thanks go to the program committee and the external reviewers.
ii We are also grateful to the FLoC 2018 organisers for their support and for hosting the workshop, and we are indebted to the EasyChair team for the availability of the EasyChair Conference System.
Dynamic Strategy Priority: Empower the strong and abandon the weak . .
Michael Rawson and Giles Reger TFX: The TPTP Extended Typed First-order Form . . . . . . . . . . . . . . . . . . .
Geo↵ Sutcli↵e and Evgenii Kotelnikov
Simon Cruanes Pascal Fontaine Martin Giese Alberto Griggio Marijn Heule Dejan Jovanovi´c Chantal Keller Boris Konev Konstantin Korovin Laura Kovacs Cl´audia Nalon Jens Otten Giles Reger Andrew Reynolds Philipp Ruemmer Martin Suda Mattias Ulbrich Josef Urban
Aesthetic Integration Loria, INRIA, University of Lorraine University of Oslo Fondazione Bruno Kessler The University of Texas at Austin SRI International LRI, Universit´e Paris-Sud University of Liverpool The University of Manchester Vienna University of Technology University of Bras´ılia University of Oslo The University of Manchester University of Iowa Uppsala University Vienna University of Technology Karlsruhe Institute of Technology Czech Technical University in Prague Additional Reviewers