Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Tue, 19 Oct 93 12:10:19 MET
From: schneide <schneide@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: FAUST and Extensions
Message-Id: <"iraun1.ira.214:19.09.93.11.07.37"@ira.uka.de>

Wishnu Prasetya has said:
> (1) Can anyone tell me how to get a copy of FAUST?

D. Shepherd answered correctly:
|> I think its ftp-able from
|> 
|> 	goethe.ira.uka.de

Wishnu Prasetya also asked:
|> (2) How fast FAUST can prove the following:
|>  
|>        "(?!x. x=f(g x)) = (?!y. y=g(f y))"

Simon Finn answered correctly:
|> As I understand it, there's a more fundamental limitation.
|> FAUST works with pure first-order logic, but for this proof
|> you need first-order logic *with equality*.


The current version which is ftp-able from goethe.ira.uka.de
is only an experimental version which supports pure first-order
logic without equality or sorts. It is possible to extend the 
prover both by equality and by sorts, but we are not interested
in such an extension. At the moment, we are more interested in
extensions which are more important for hardware verification 
and this is at the moment the proof power of FAUST. The prover
is not as powerful as it could be although the HOL90 version is
about 40 times faster than the elderly HOL88 version (which is
no more available). We investigate therefore in further enhancements,
the most drastic ones have been presented at the CHDL in Ottawa
this year (the paper is also available by ftp from goethe.ira.uka.de.
 A mixture of the tableau graphs presented on the HOL workshop in
Leuven and the well known BDDs is used in the new implementation. 
However, as there is an industrial interest, it is unclear at the 
moment, if this version will also be public domain. 
  Another extension (and this is the most interesting one) is the
extension of FAUSTs intantiation mechanism. At the moment only
Robinson's first-order unification is used, but it can be 
exchanged by other unification algorithms, e.g. higher-order 
unification (as it is used in LAMBDA) or some kinds of 
theory unification (which makes FAUST domain specific).
The latter extension seems very interesting for further
research in this area.


Klaus