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 -