=Paper=
{{Paper
|id=Vol-2162/preface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2162/preface.pdf
|volume=Vol-2162
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-2162/preface.pdf</pdf>
<pre>
                 PAAR-2018
            Sixth Workshop on
Practical Aspects of Automated Reasoning

                    July 19, 2018

  Affiliated with the Federated Logic Conference 2018




                     Oxford, UK
Preface

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 dis-
cuss 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 implemen-
tation 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 non-
   classical logics;
 – implementation of provers (SAT, SMT, resolution, tableau, instantiation-
   based, rewriting, logical frameworks, etc.);
 – automated reasoning tools for all kinds of practical problems and applica-
   tions;
 – 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 heuris-
   tics, 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.


July 2018                                                           Boris Konev
Liverpool, Prague, Uppsala                                           Josef Urban
                                                                Philipp Rümmer




                                        iii
Table of Contents

The CakeML Verified Compiler and Toolchain . . . . . . . . . . . . . . . . . . . . . . . .                                     1
   Magnus O. Myreen
Set of Support for Higher-Order Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . .                                2
   Ahmed Bhayat and Giles Reger

Efficient translation of sequent calculus proofs into natural deduction
proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .   17
    Gabriel Ebner and Matthias Schlaipfer
Evaluating Pre-Processing Techniques for the Separated Normal Form
for Temporal Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .              34
    Ullrich Hustadt, Cláudia Nalon and Clare Dixon
Proof Search Optimizations for Non-clausal Connection Calculi . . . . . . . . .                                                49
   Jens Otten
Dynamic Strategy Priority: Empower the strong and abandon the weak . .                                                         58
  Michael Rawson and Giles Reger
TFX: The TPTP Extended Typed First-order Form . . . . . . . . . . . . . . . . . . .                                            72
  Geo↵ Sutcli↵e and Evgenii Kotelnikov
A Verified Simple Prover for First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . .                                 88
   Jørgen Villadsen, Anders Schlichtkrull and Andreas Halkjær From




                                                                iv
Program Committee

Haniel Barbosa       University of Iowa
Simon Cruanes        Aesthetic Integration
Pascal Fontaine      Loria, INRIA, University of Lorraine
Martin Giese         University of Oslo
Alberto Griggio      Fondazione Bruno Kessler
Marijn Heule         The University of Texas at Austin
Dejan Jovanović     SRI International
Chantal Keller       LRI, Université Paris-Sud
Boris Konev          University of Liverpool
Konstantin Korovin   The University of Manchester
Laura Kovacs         Vienna University of Technology
Cláudia Nalon       University of Brası́lia
Jens Otten           University of Oslo
Giles Reger          The University of Manchester
Andrew Reynolds      University of Iowa
Philipp Ruemmer      Uppsala University
Martin Suda          Vienna University of Technology
Mattias Ulbrich      Karlsruhe Institute of Technology
Josef Urban          Czech Technical University in Prague


Additional Reviewers
Schurr, Hans-Jörg




                              v

</pre>