Challenges and Novel Applications for Automated Reasoning

CADE-19 Workshop
July 28, 2003
Miami
USA

Outline:

The aim of this workshop is to identify some grand challenges and novel applications that will fire the imaginations of both new researchers arriving into AR as well those already long established in the field. The main application at present for automated reasoning has been for reasoning about computer systems (in particular, software and hardware verification). One of the goals of this workshop are to identify and promote other more novel application areas such as bioinformatics and the semantic web, as well as to identify challenges that may one day become important applications. The tradition of grand challenges is common in many branches of science. Some examples of grand challenges within computer science include: to prove whether P = NP (open), to develop a world class chess program (completed, 1990s), or to automatically translate Russian into English (failed, 1960s). Such challenges help determine the fundamental limits of computation, as well as often capturing the imagination of scientists and the public alike.

The UK Computing Research Committee has proposed a set of criteria for assessing grand challenges in computing which can be applied to grand challenges in automated reasoning. There is no expectation that grand challenges will meet all of these criteria, but they is an expectation that they will meet some of them:

• It arises from scientific curiosity about the foundation, the nature or the limits of the discipline.
• It gives scope for engineering ambition to build something that has never been seen before.
• It will be obvious how far and when the challenge has been met (or not).
• It has enthusiastic support from (almost) the entire research community, even those who do not participate and do not benefit from it.
• It has international scope: participation would increase the research profile of a nation.
• It is generally comprehensible, and captures the imagination of the general public, as well as the esteem of scientists in other disciplines.
• It was formulated long ago, and still stands.
• It promises to go beyond what is initially possible, and requires development of understanding, techniques and tools unknown at the start of the project.
• It calls for planned co-operation among identified research teams and communities.
• It encourages and benefits from competition among individuals and teams, with clear criteria on who is winning, or who has won.
• It decomposes into identified intermediate research goals, whose achievement brings scientific or economic benefit, even if the project as a whole fails.
• It will lead to radical paradigm shift, breaking free from the dead hand of legacy.
• It is not likely to be met simply from commercially motivated evolutionary advance.