1.-2. April 1996
This workshop was not organised as a mini-conference, but in order to stimulate discussions among the 30-35 attendees, in form of two invited talks, four panel discussions, a demo session, and a poster session. Of the four panels, I only describe the first in detail, since the arguments are of general interest, even beyond the area of automated reasoning.
Invited Talk by Jean-François Puget The first invited talk was given by Puget (ILOG) on the applications of techniques for solving constraint satisfaction problems or constraint optimisation problems. This talk was sponsored by the COMPULOG net. Typical applications are scheduling problems of airports, transport scenarios and time tabling problems. Since constraint satisfaction problems are essentially equivalent to propositional logic, the general problem is NP-complete and hence too hard for real world cases. In order to overcome this problem, special efficient incomplete consistency checks have been developed and successfully used.
Panel: Bridging the gap The following panel with Chris Preist (chair), Alan Bundy, Chris Price, Jean-François Puget had the title: ``Bridging the gap between industry, academia, and government''.
Bundy pointed out that in the future it will become more and more important to have industrial collaborators in order to get grants. Such collaborators can provide tough test examples which can be the acid test of whether the ideas really work. In order to make contact it is necessary to attend related conferences and to make visits. Finding possible applications of automated reasoning often requires imagination and flexibility. The risk of potential collaborations can be minimised by low-risk start-ups like student projects.
Price compared the situation of nowadays scientists to that of musicians like Bach who needed patrons for his work. In particular we can learn from their way of getting money: we have to promise what the patron wants, we have to deliver on the promises, we have to take the collaborator's limitation into account, and we have to be grateful.
Puget compared the different terms on which industry and science work have to work (products vs. prototypes, property vs. publication, practical problems vs. theory, development time of less than 18 months vs. three years). Furthermore in a commercial product only 15% of the total effort is devoted to the proper problem solving facility (50% graphics, 20% applications, 15% data bases).
Preist stressed that industrialists and academics must accept each other as equal partners and compromise to help the other to succeed (work with, not for). Otherwise a disaster scenario is possible, where industrialists expect academics to the work of their R&D department and academics expect to get paid for what they feel like.
The discussion was partly concerned with the question how a fast transmission of knowledge can be achieved and how the links between pure research, applied academic research, applied industrial research, and product R&D can be strengthened.
Panel: Temporal Reasoning
The second panel with Michael Fisher (chair), Clare Dixon, Rob Johnson, Fabio Massacci, and André Trudel was devoted to ``Implementing Temporal Reasoning''. In this panel, the most interesting question that goes beyond the direct field of temporal reasoning was how to overcome the general all-or-nothing situations in theorem proving.
Invited Talk by Howard Barringer
In his talk Barringer presented the propositional temporal logic TDTL, which is built up using two temporal operators, namely a binary ``unless'' operator and a unary ``next'' operator. Many other operators can be defined in terms of ``unless'' and ``next''. For this logic exists a decidable calculus. If the TDTL language is restricted so that only certain combinations of temporal operators can be combined, the computational effort for evaluating expressions is polynomial in the size of the formula. The main applications are in program verification for finite state programs and in natural language processing.
Panel: Usability of Automated Reasoning In the third panel, with Helen Lowe (chair), Stuart Aitken, Judith Underwood, and Nick Merriam, aspects of user interfaces, of automation in interactive theorem proving, and of the advantages and disadvantages of different logical formalisms were discussed.
Open Session In the last session, chaired by Ian Gent, who was the programme chair of the whole workshop, everybody could hand in his/her favourite topic. Topics were: standardising the input/output of theorem provers, the relevance of theory for applications, and the most promising/exciting application areas for automated reasoning in the next decade.
Report by: Manfred Kerber, The University of Birmingham, e-mail: M.Kerber@cs.bham.ac.uk
A PostScript version can be found here.