=Paper=
{{Paper
|id=Vol-2752/xpreface
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2752/xpreface.pdf
|volume=Vol-2752
}}
==None==
https://ceur-ws.org/Vol-2752/xpreface.pdf
PAAR-2020
Seventh Workshop on
Practical Aspects of Automated Reasoning
June 29-30, 2020
http://www.eprover.org/EVENTS/PAAR-2020.html
SC2 -2020
Fifth Workshop on
Symbolic Computation and Satisfiability Checking
July 5, 2020
http://www.sc-square.org/CSA/workshop5.html
Affiliated with the
10th International Joint Conference on Automated Reasoning
(IJCAR 2020)
Virtual (originally Paris, France)
Preface
This volume contains the papers presented at the Seventh Workshop on Practical Aspects of Automated Reason-
ing (PAAR-2020) and at the Fifth Workshop on Satisfiability Checking and Symbolic Computation (SC2 -2020).
The workshops were held respectively on June 29–30, 2020, and on July 5, 2020, virtually, in association with
the Tenth International Joint Conference on Automated Reasoning (IJCAR-2020).
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. The purpose of PAAR is to help the community
understand how to build useful and powerful reasoning systems in practice, and how to apply existing systems
to real problems.
PAAR received nineteen submissions. Each submission was reviewed by at least three program committee
members. Sixteen papers were accepted for presentation, and the workshop was extended from one day to two
days to accommodate for the unexpectedly high number of presentations. Thirteen papers were invited for the
proceedings; in the end, twelve papers could be included in the proceedings.
The aim of the SC2 workshop is to provide an opportunity to discuss, share knowledge and experience across
two communities: symbolic computation and satisfiability checking. Symbolic computation is concerned with
the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiabil-
ity Checking has recently started to tackle similar problems but with different algorithmic and technological
solutions.
SC2 received three papers, each of which received three reviews by the members of the programme committee.
We attribute low submission rate to disruptions caused by COVID-19. Nevertheless, all submitted papers were
of high quality and were accepted for presentation at the workshop and publication in this volume.
The PAAR and SC2 workshop organizers would like to thank the authors and participants of both workshops
for making two very successful events possible, particularly in these special COVID-19 times. Our thanks also go
to the program committee members and the external reviewers for their considerable effort to provide thorough
and constructive reviews. As in all years, we are indebted to the EasyChair team for the unfailing availability of
the EasyChair Conference System. We are grateful to the CEUR team for publishing our proceedings. The SC2
workshop organizers would like to thank the SMT-2020 workshop for accommodating a joint SC2 /SMT session.
Last but not least, the IJCAR organizers were extremely helpful in finding good solutions to still have the
workshops in spite of the 2020 sanitary crisis. The PAAR and SC2 workshop chairs are very grateful to them
for their support and for virtually hosting the workshops.
November 2020 Konstantin Korovin and Ilias S. Kotsireas (SC2 Chairs)
Pascal Fontaine, Philipp Rümmer, Sophie Tourret (PAAR Chairs)
II
Program Committee (PAAR)
Simon Cruanes Aesthetic Integration, Texas, USA
Hans de Nivelle Nazarbayev University, Kazakhstan
Bruno Dutertre SRI international, California, USA
Gabriel Ebner VU Amsterdam, Netherlands
Pascal Fontaine (co-chair) Liège University, Belgium
Antti Hyvärinen University of Lugano, Switzerland
Ahmed Irfan Stanford University, California, USA
Cezary Kaliszyk University of Innsbruck, Austria
Daniel Le Berre CNRS - University of Artois, France
Ondrej Lengal Brno University of Technology, Czech Republic
Tomer Libal American University of Paris, France
Cláudia Nalon University of Brası́lia, Brasil
Jens Otten University of Oslo, Norway
Philipp Rümmer (co-chair) Uppsala University, Sweden
Renate A. Schmidt The University of Manchester, UK
Stephan Schulz DHBW Stuttgart, Germany
Martina Seidl Johannes Kepler University Linz, Austria
Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France
Alexander Steen University of Luxembourg, Luxembourg
Martin Suda Czech Technical University, Czech Republic
Geoff Sutcliffe University of Miami, Florida, USA
Sophie Tourret (co-chair) Max-Planck Institute for Informatics, Germany
Sarah Winkler University of Verona, Italy
Aleksandar Zeljić Stanford University, California, USA
Program Committee (SC2 )
John Abbott Università degli Studi di Genova, Italy
Erika Abraham RWTH Aachen University, Germany
Anna M. Bigatti Universita di Genova, Italy
Curtis Bright University of Waterloo
James H. Davenport University of Bath, U.K.
Matthew England Coventry University, UK
Pascal Fontaine Liège University, Belgium
Vijay Ganesh University of Waterloo, Canada
Alberto Griggio Fondazione Bruno Kessler, Trento, Italy
Marijn J.H. Heule Carnegie Mellon University, USA
Ahmed Irfan Stanford, USA
Dejan Jovanovic SRI, USA
Manuel Kauers Johannes Kepler University, Linz, Austria
Konstantin Korovin (co-chair) The University of Manchester, UK
Ilias S. Kotsireas (co-chair) Wilfrid Laurier University, Canada
Laura Kovacs TU Wien, Austria
David Monniaux University of Grenoble, France
Norbert Mueller University of Trier, Germany
Stefan Ratschan Academy of Sciences of the Czech Republic, Prague, Czech Republic
Martina Seidl Johannes Kepler University, Linz, Austria
Thomas Sturm CNRS, Nancy, France and MPI Informatik, Germany
III
Table of Contents
Workshop on Practical Aspects of Automated Reasoning 2020
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form . . . . . . . . . . . . . . . . 1
Pedro Barroso, Mario Pereira and António Ravara
Learning Precedences from Simple Symbol Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Filip Bártek and Martin Suda
Layered Clause Selection for Saturation-Based Theorem Proving . . . . . . . . . . . . . . . . . . . . . . . 34
Bernhard Gleiss and Martin Suda
Simplifying Casts and Coercions (Extended Abstract) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
Robert Y. Lewis and Paul-Nicolas Madelaine
Evaluation of Axiom Selection Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
Qinghua Liu, Zishi Wu, Zihao Wang and Geoff Sutcliffe
Equality Preprocessing in Connection Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
Benjamin E. Oliver and Jens Otten
Give Reasoning a Trie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
Thomas Prokosch and François Bry
Directed Graph Networks for Logical Reasoning (Extended Abstract) . . . . . . . . . . . . . . . . . . . . 109
Michael Rawson and Giles Reger
Efficient Implementation of Large-Scale Watchlists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
Constantin Ruhdorfer and Stephan Schulz
Cutting Down the TPTP Language (And Others) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
Nahku Saidy, Hanna Siegfried, Stephan Schulz and Geoff Sutcliffe
Boolean Reasoning in a Higher-Order Superposition Prover . . . . . . . . . . . . . . . . . . . . . . . . . . 148
Petar Vukmirović and Visa Nummelin
Querying the Guarded Fragment via Resolution (Extended Abstract) . . . . . . . . . . . . . . . . . . . . 167
Sen Zheng and Renate A. Schmidt
Satisfiability Checking and Symbolic Computation Workshop 2020
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract) . . . . . 178
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer and Zak Tonks
Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers . . . . . . . . . . . . 189
Christoph Lüders
GeoGebra and the realgeom Reasoning Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204
Róbert Vajda and Zoltán Kovács
IV