Abstract
This Special Issue on Automated Reasoning follows two successful events in Automated Reasoning: The First Conference on Artificial Intelligence and Theorem Proving1
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
Both participants of AITP 2016 and PAAR 2016, as well as members of the larger community were invited to submit contributions.
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