You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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 Proving1 (AITP 2016) and The Fifth Workshop on Practical Aspects of Automated Reasoning2 (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

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

Special Issue Reviewers

Michael BeesonSan José State University
Maria Paola BonacinaUniversity of Verona
Joachim BreitnerUniversity of Pennsylvania
James BrotherstonUniversity College London
Matthew EnglandCoventry University
Vijay GaneshUniversity of Waterloo
Sean HoldenUniversity of Cambridge
Johannes HölzlCarnegie Mellon University
Mikoláš JanotaUniversity of Lisbon
Manfred KerberUniversity of Birmingham
Alexander LeitschTU Wien
Bertrand MazureUniversité d’Artois
Hans de NivelleUniversity of Wrocław
Lawrence PaulsonUniversity of Cambridge
Michael NorrishData61 and Australian National University
Andrei PopescuMiddlesex University London
Giles RegerUniversity of Manchester
Gerhard SchellhornUniversität Augsburg
Pascal SchreckUniversity of Strasbourg
Martin StreckerUniversité Paul Sabatier
Geoff SutcliffeUniversity of Miami
Ivan VarzinczakUniversité d’Artois
Jiří VyskočilCzech Technical University in Prague
Uwe WaldmannMPI Saarbrucken