http://www.eprover.org/EVENTS/PAAR-2020.html This volume contains the papers presented at the Seventh Workshop on Practical Aspects of Automated Reasoning (PAAR-2020) and at the Fifth Workshop on Satis ability 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 di erent implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brings together di erent groups to concentrate on practical aspects of the implementation and application 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 satis ability checking. Symbolic computation is concerned with the e cient algorithmic determination of exact solutions to complicated mathematical problems. Satis ability Checking has recently started to tackle similar problems but with di erent 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 e ort 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 nding 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 Rummer, Sophie Tourret (PAAR Chairs)
III
Learning Precedences from Simple Symbol Features : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 21
Filip Bartek and Martin Suda Give Reasoning a Trie : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 93
Thomas Prokosch and Francois Bry
Computing Tropical Prevarieties With Satis ability Modulo Theories (SMT) Solvers : : : : : : : : : : : : 189
Christoph Luders GeoGebra and the realgeom Reasoning Tool : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 204 Robert Vajda and Zoltan Kovacs