Foreword to the Special Issue on Automated Reasoning
This Special Issue on Automated Reasoning follows two successful events in Automated Reasoning: The First Conference on Artificial Intelligence and Theorem Proving11 (AITP 2016) and The Fifth Workshop on Practical Aspects of Automated Reasoning22 (PAAR 2016). The PAAR workshop was held on July 2, 2016, in Coimbra, Portugal, in association with the Eighth International Joint Conference on Automated Reasoning (IJCAR-2016). AITP 2016 took place from April 3 to April 7, 2016, in Obergurgl, Austria.
PAAR is a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. PAAR brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools.
AITP is a new series of discussion-oriented conferences focusing on combinations of AI, machine learning, linguistic and reasoning methods and tools deployed over large mathematical and scientific corpora. It grew out of our strong impression that large-scale semantic processing and computer assistance of mathematics and science is an inevitable part of our future. AITP strives to provide a forum for discussing how to get there as soon as possible and driving the progress towards that.
The focus of the special issue are new combination of AI and Automated Reasoning, and practical applications of Automated Reasoning. More specifically, some suggested topics were:
Automated reasoning in propositional, first-order, higher-order and non-classical logics
AI and big-data methods in theorem proving and mathematics
Collaboration between automated and interactive theorem proving
Alignment and joint processing of formal, semi-formal, and informal libraries
Implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frameworks, etc)
Automated reasoning tools for all kinds of practical problems and applications
Methods for large-scale computer understanding of mathematics and science
Common-sense reasoning and reasoning in science
Combinations of linguistic/learning-based and semantic/reasoning methods
Pragmatics of automated reasoning within 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, optimizations techniques, strategies and heuristics, fairness
The special issue received fifteen submissions. The submissions were peer-reviewed using the standard refereeing procedure of AI Communications, and four papers were accepted for inclusion into the special issue. The papers cover a broad area, with topics ranging from improved techniques for SAT and AI methods for first-order reasoning to proof verification, and toolchains for solving university entrance exams.
We would like to thank the authors of all submissions for considering this special issue, and the special issue reviewers for their considerable effort to provide high-quality reviews. As PAAR and AITP organizers we would also like to thank the participants of both events for helping to make them successful. Our thanks also go the program committees and the external reviewers of these events. AITP’16 was partially supported by the ERC grant no. 649043 AI4REASON.
Pascal Fontaine
Cezary Kaliszyk
Stephan Schulz
Josef Urban
Special Issue Reviewers
| Michael Beeson | San José State University |
| Maria Paola Bonacina | University of Verona |
| Joachim Breitner | University of Pennsylvania |
| James Brotherston | University College London |
| Matthew England | Coventry University |
| Vijay Ganesh | University of Waterloo |
| Sean Holden | University of Cambridge |
| Johannes Hölzl | Carnegie Mellon University |
| Mikoláš Janota | University of Lisbon |
| Manfred Kerber | University of Birmingham |
| Alexander Leitsch | TU Wien |
| Bertrand Mazure | Université d’Artois |
| Hans de Nivelle | University of Wrocław |
| Lawrence Paulson | University of Cambridge |
| Michael Norrish | Data61 and Australian National University |
| Andrei Popescu | Middlesex University London |
| Giles Reger | University of Manchester |
| Gerhard Schellhorn | Universität Augsburg |
| Pascal Schreck | University of Strasbourg |
| Martin Strecker | Université Paul Sabatier |
| Geoff Sutcliffe | University of Miami |
| Ivan Varzinczak | Université d’Artois |
| Jiří Vyskočil | Czech Technical University in Prague |
| Uwe Waldmann | MPI Saarbrucken |