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 -