REPORT ON ANU/ICOT COOPERATION Michael McRobbie Executive Director Centre for Information Science Research The Australian National University 1 Introduction Unlike many of the other participants in the Evaluation Workshop I do not feel competent to evaluate or comment in detail on the research activities of ICOT over the 10 years of the project though I will provide some general comments later in this report. ANU's position is different to that of many other organizations that have co- operated and collaborated with ICOT in that our interaction is almost solely in an application area - theorem proving - and not at the level of the fundamental research that has been until recently ICOT's main focus. Further our interaction only really commenced in 1992 though it has grow quickly into a valuable collaboration that has rapidly yielded significant results. Thus I will restrict myself to describing this interaction and commenting on the quality of ICOT's work in theorem proving 2 History ANU followed with great interest the MITI initiative that became ICOT from about 1980 and followed in broad outline the activities of ICOT ever since. ANU has had a strong logic research group since the early 1970s and this group started working in theorem proving about 10 years ago. The announcement in the early 1980s that Japan was to initiate a major well funded initiative in logic-based computer systems was an enormously exciting one to members of this group and it is difficult to convey now just how galvanizing an effect it had on researchers in foreign countries who had been working on computing and logic for years in relative obscurity. ICOT was a major stimulus not just to their morale but also to the establishment of large, well funded programs and laboratories in many foreign countries such as Alvey, Esprit, MCC and SICS. These facts are well known and I will not dwell on them as others more knowledge- able than I will certainly do so in their reports. However the involvement of research institutions in my country, Australia, with ICOT, is less well known and is worth briefly putting on the record since this report is being written at the last FGCS Conference. - 76 - In the early 1980s there was an exceptionally strong research group in logic pro- gramming at the University of Melbourne led by John-Louis Lassez and containing John Lloyd, Rao, and others. As I understand it the Australian Minister for Science visited ICOT around 1983 or 84 and heard many favourable things about the research of the University of Melbourne group. He returned to Australia and made a decision to fund a "Machine Intelligence Project" based on the logic programming group at the University of Melbourne. The level of funding was good by the standards of the time, but unfortunately the huge amount of international interest that was generated by ICOT in logic programming and related areas caused talent in this area to be at an absolute premium. Hence it was not long before many members of this exceptional group had accepted much more attractive positions overseas. I believe from informal discussions with a number of these people over the years, many of them would have quite happily stayed at the University of Melbourne and hence brought great distinction to the University of Melbourne and to Australia.[1] However a combination of an inflexible university system (since improved somewhat) and a lack of any sort of understanding of the emerging importance of the field of logic programming on the part of various government decision makers meant that a significant opportunity to establish a stable group of international stature in this area was unfortunately lost. Researchers from a number of other Australian research organizations had various interactions over the years with ICOT but that with the University of Melbourne was the most substantial of them. ANU took an initiative around 1987 to establish what is in effect the national centre for high performance computing and now has 4 supercomputers - 2 Japanese and 2 American. This initiative was numerically based but because of ANU's long-standing interest in logic and theorem proving as well as ICOT's announcement at the 1988 FGCS conference of the plan to build the PIM machines, ANU decided to explore with ICOT the possibility of establishing some sort of agreement on research cooperation. Discussions commenced in 1989, initially with Dr Kurozumi and then also with Dr Uchida, in tandem with discussions to have ICOT participate in the 11th International Joint Conference on Artificial Intelligence which was to be held in Sydney in August, 1991. In 1991 a series of letters was exchanged between the Centre I head at ANU and ICOT to establish research cooperation in the field of theorem proving. Following ICOT's very successful participation in IJCAI-91, a party of about 30 ICOT scientists ------------------------------------------------------- [1] An example of what could have been is nicely seen in the fact that the 4th International Logic Programming Conference was held at the University of Melbourne in 1987. A major international event in logic and computing with a heavy emphasis on logic programming co-sponsored by the University of Melbourne was also held in Melbourne in early 1984. - 77 - travelled to ANU In September 1991 to install two Psi-2 workstations and to give a wide ranging series of lectures on ICOT's research. Dr Uchida has since indicated that the Psi-2 workstations which have been very difficult to maintain properly will be re- placed by the more reliable, powerful and more standard Psi-3 workstations soon after FGCS-92 is finished. 3 ANU/ICOT Cooperation For various reasons cooperation between ANU and ICOT only really began in early 1992. The cooperation has so far just been limited to theorem proving and has mainly involved Drs Slaney and Grundy at ANU and Drs Hasegawa, Fujita and Koshimura at ICOT. The cooperation has so far been in three different areas: (i) heterogeneous high performance theorem proving systems (ii) application of model generation techniques in theorem proving and (iii) system independent theorem prover performance analysis tools. (i) Heterogeneous High Performance Theorem Proving Systems In 1991 Dr John Slaney of ANU and Dr Ewing Lusk of Argonne National Labo- ratory (ANL) in the United States devised a new automated theorem proving system called SCOTT for Semantically Constrained Otter - Otter being a high performance theorem prover written by Dr Bill McCune at Argonne National Laboratory which is generally regarded as the fastest and best general purpose theorem prover presently in existence. On a wide variety of problems SCOTT is about twice as fast as Otter. SCOTT builds into Otter the well known and venerable principal of semantic res- olution which uses a model of the underlying theory with which the theorem prover is working to help guide the search for a proof. However semantic resolution is a static principal in that it uses a model, usually arrived at by somewhat arbitrary and non- systematic methods, and once incorporated into a theorem prover this model is not changed for the duration of the search for a proof. The key new idea in SCOTT is that as in a standard resolution theorem prover it starts with a model of the underlying theory. However as more information is built up about this theory as the search for a proof progresses, this in turn Is used to generate dynamically new and more precise models for the theory that both guide the search for a proof more effectively and which decrease the number of clauses that are discarded by expensive methods such a subsumption. The techniques used to dynamically gen- erate such models systematically and efficiently given that the problem is exponential in its order of complexity in the number of values in the model, were developed over 10 years by Slaney and others mainly at ANU. Much of Slaney's work in this area is embodied In the program FlNDER (available by anonymous ftp from arp.anu.edu.au). - 78 - SCOTT then in effect integrates together Otter, FINDER, a model testing module (in this case really just a module of FINDER) and a new performance monitoring tool called XSCGraph developed by Grundy which we discuss under (iii)below. All these programs are written in C. Following the visit to ANU of the ICOT party in 1991, Slaney and Grundy noticed that ICOT' s grounded MGTP theorem prover and their non-ground version developed primarily by Drs Hasegawa and Fujita, could be combined together in the same way as Finder and Otter are combined respectively. What was necessary was to build the testing interface between them. This has been written in KL-1 by Grundy working at ICOT over the last 2 months. The combined system called Semantically Constrained MGTP (SC/MGTP) is all written in KL-1 and runs on Psi-3 workstations. Work has begun to implement it on the 256 Processor Mitsubishi Electric Corporation PIM-m. SC/MGTP runs about 4 times faster than Otter running on a Sparcstation 1, and given that each processor in the PIM-m is effectively a Psi-3 processor, there is the potential for SC/MGTP to run hundreds of times faster than Otter. However I stress that this research has only just begun and that those working on it have not yet had time to analyse the comparative performance of the systems in any depth. Thus some of the figures just mentioned are to a certain extent conjectural. (ii) Application of Model Generation Techniques in Theorem Proving The topic here is rather technical but in brief it is a collaboration between ANU using the Finder system and ICOT using the ground-MGTP system to attack a series of problems posed by Bennett concerning certain finite algebraic structures in group theory. These problem have so far resisted solution by any automated theorem prover but a number of them have now been solved using Finder and ground-MGTP. This work was announced at FGCS-92 and will be reported on in detail in a joint paper by Hasegawa, Fujita and Slaney. To paraphrase Lusk and Slaney from their CADE-92 tutorial on Finding Models, these result are more than a little encouraging and at the very least indicate that there is a rich vein of open mathematical problems concerning finite algebraic structures which can now be approached by means of automated reasoning techniques. (iii) System Independent Theorem Prover Performance Analysis Tools A regular criticism heard of some of ICOT's work is that without comparisons with other international research in the same fields it is difficult to form an appreciation of how good the work really is. As part of the collaboration to build SC/MGTP a system independent performance analysis tool XSCGraph has been written by Grundy - 79 - specifically to allow the direct comparison of the performance of the C-based SCOTT system and the KL-1-based SC/MGTP system, as well as many other systems. It is clear from (ii) that SC/MGTP compares very favourably with SCOTT and XSCGraph allows a more detailed comparison to be made on how they perform on the same problems. 4 Comments on ICOT Research on Theorem Proving I hope that my discussion in the previous section indicates first that the collabo- ration between ANU and ICOT has grown in a short time to be a very fruitful one and one that parallels and complements in a close way the collaborative relationship between ANU and ANL. It should also be clear that the ICOT work on theorem proving stands favourable comparison with some of the world's best which can be seen from the fact that it has passed the hardest test of all - proving a significant open mathematical problem. The ANU researchers involved in the collaboration have also reported favourably on KL-1 as a prototyping language. The ANU/ICOT achievements were cited prominently a number of times during FGCS-92 and all the research discussed in Section 3 was either demonstrated at the FGCS Demonstration or reported on at the Conference. 5 The Future ANU has been very pleased with how Its collaboration with ICOT has progressed in 1992. Because of this we will be employing another researcher to work on the joint research projects and to help maintain the Psi-3 workstations once they arrive. We certainly support the idea of the core activities in ICOT being extended beyond March, 1993. Making ICOT tools such as KL-1 available on "stock" Unix platforms would be a great advantage and ICOT should be encouraged to do so as soon as possible. - 80 -