LAUSR

On March 8, 2018, Tobias Nipkow celebrated his sixtieth birthday. In anticipation of the occasion, after some discussion in early 2016 among all the editors of the Journal of Automated Reasoning except Tobias, it was decided to create two special issues to honor Tobias contributions to automated reasoning and their influence on the field. The first issue, which has already appeared in Volume 61 under the title Introduction to Milestones in Interactive Theorem Proving, includes a synopsis on Tobias’s scientific life. In addition to his influence on interactive theorem proving, which was the focus of the first special issue, this special issue honors his influence on automated reasoning as well. Interactive theorem proving, and in particular the Isabelle proof assistant co-developed by Tobias’s research group, have turned out to be a major success story for automatic reasoning itself. The need to improve automatic reasoning procedures to be used by interactive theorem provers to increase their own level of automation has led to an essential and vibrant new research direction in which Tobias and his close collaborators have played a crucial role so far. To honor that role this special issue is dedicated specifically to automated reasoning systems, as stated in its call for papers.