Collaborative reasoning

Although our critics have proved very successful there are situations in which they can only construct a partial proof patch. Allowing the user to interact with the critics mechanism in such situations will ultimately increase the overall power and robustness of the proof planning approach to building theorem provers, i.e. complement the existing machine critics by making provision for human critics.

We have built an interactive proof planner [8] in which the user interacts through proof critics. This allows the user to collaborate on the analysis of proof failures and the synthesis of proof patches. Early evaluation of the planner has proved positive [6], further studies are underway at Napier University.

Given current tool support, there still exists a skills bottle-neck in terms of the application of formal methods to the design of computer systems. One approach to addressing this ``bottle-neck'' is to increase the level of automation. In general, however, aiming exclusively for automation will significantly limit the applicability of tools. What is required is a level of interaction which is closer to the needs of the user, i.e. the systems designer. We believe that our interactive proof critics makes a real contribution in this area.