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 -