Vol-2752
urn:nbn:de:0074-2752-0

Copyright © 2020 for the individual papers by the papers' authors. Copyright © 2020 for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).

PAAR+SC-Square 2020
Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020

Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020
co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020)

Paris, France, June-July, 2020 (Virtual).

Edited by

Pascal Fontaine *
Konstantin Korovin
Ilias S. Kotsireas *
Philipp Rümmer
Sophie Tourret *

* University of Liège, Faculty of Applied Sciences, Liège, Belgium
** The University of Manchester, School of Computer Science, Manchester, UK
*** Wilfrid Laurier University, Department of Physics and Computer Science, Waterloo, Canada
**** Uppsala University, Department of Information Technology, Uppsala, Sweden
***** Max Planck Institute for Informatics, Saarbrücken, Germany

Table of Contents

Preface
Summary: For PAAR, there were 19 papers submitted for peer-review. Out of these, 13 papers were invited for this volume, 12 could be included. For SC-square, three papers were submitted for peer-review, were accepted, and are included in the current proceedings.

Workshop on Practical Aspects of Automated Reasoning 2020

Animated Logic: Correct Functional Conversion to Conjunctive Normal Form 1-20
Pedro Barroso, Mario Pereira, António Ravara
Learning Precedences from Simple Symbol Features 21-33
Filip Bártek, Martin Suda
Layered Clause Selection for Saturation-Based Theorem Proving 34-52
Bernhard Gleiss, Martin Suda
Simplifying Casts and Coercions (Extended Abstract) 53-62
Robert Y. Lewis, Paul-Nicolas Madelaine
Evaluation of Axiom Selection Techniques 63-75
Qinghua Liu, Zishi Wu, Zihao Wang, Geoff Sutcliffe
Equality Preprocessing in Connection Calculi 76-92
Benjamin E. Oliver, Jens Otten
Give Reasoning a Trie 93-108
Thomas Prokosch, François Bry
Directed Graph Networks for Logical Reasoning (Extended Abstract) 109-119
Michael Rawson, Giles Reger
Efficient Implementation of Large-Scale Watchlists 120-133
Constantin Ruhdorfer, Stephan Schulz
Cutting Down the TPTP Language (And Others) 134-147
Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe
Boolean Reasoning in a Higher-Order Superposition Prover 148-166
Petar Vukmirović, Visa Nummelin
Querying the Guarded Fragment via Resolution (Extended Abstract) 167-177
Sen Zheng, Renate A. Schmidt

Satisfiability Checking and Symbolic Computation Workshop 2020

New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract) 178-188
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks
Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers 189-203
Christoph Lüders
GeoGebra and the realgeom Reasoning Tool 204-219
Róbert Vajda, Zoltán Kovács

2020-11-18: submitted by Pascal Fontaine metadata incl. bibliographic data published under Creative Commons CC0
2020-11-26: published on CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073) |valid HTML5|