Special issue on practical aspects of automated reasoning
Boris Yur'evich Konev, Renate A. Schmidt, Stephan Schulz · AI Communications · 2010
Automated reasoning is one of the most exciting fields of research in computer science. It provides the ability to apply the speed, precision and endurance of computers to tedious tasks that currently require exquisitely trained and highly skilled human experts. Successful automated reasoning systems can ensure a much higher level of trust in complex mathematical proofs, they can enable us to automatically eliminate large classes of errors from software systems and communication protocols, and they can be used to support the creation and reasoning in large knowledge bases and theories. After a long time of significant, but mostly theoretical progress, the last decade has experienced a marked increase in useful implementations and applications of reasoning systems. We are seeing some of the fruits of this practical and application oriented research now. After a number of successes by various groups in mathematical reasoning [3], hardware verification [1,4,5], and software synthesis [6], NICTA in Canberra has just announced the first fully verified operation system kernel [2]. In order to further help the transition from theory to practice we organized a number of workshops dealing with practical aspects of automated reasoning: