Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 1 Jul 1993 10:51:51 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19370;
          Thu, 1 Jul 93 02:43:23 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA19365;
          Thu, 1 Jul 93 02:43:09 -0700
Message-Id: <9307010943.AA19365@ted.cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <27188-0@iraun1.ira.uka.de>; Thu, 1 Jul 1993 11:43:23 +0200
Date: Thu, 1 Jul 93 11:45:05 MET DST
From: "Thomas Kropf, Univ. Karlsruhe" <kropf@ira.uka.de>
To: info-hol@ted.cs.uidaho.edu
Subject: FAUST-prover for HOL90

Paul Loewenstein writes:
 
> It is quite clear that more sophisticated proof procedures are required
> (and are being added) to reduce unnecessarily tedious human interaction.

> I would love to see more encouragement to make the switch, possibly
> by a policy of introducing significant new features and proof procedures
> to HOL90 first.

A public domain version of our automated first-order prover FAUST
has been made available at our ftp site goethe.ira.uka.de (129.13.18.22)
in the directory pub/software. It runs in SML and is intended to be used
together with HOL90.5. 

Further details about the underlying theory of FAUST can be found in
the literature indicated below.

That's our contribution to those "new features and proof procedures"
making life easier in HOL90 :-)

  --Thomas--

_________________________________________________________________________
@inproceedings{ScKK92b,
  crossref    ={HOL92},
  author      ={{K. Schneider} and {R. Kumar} and {Th. Kropf}},
  title       ={Efficient Representation and Computation of Tableau Proofs},
  pages       ={471--492},
  key         ={ScKK92b},
}
@article{ScKK93b,
  author    ={{K. Schneider} and {R. Kumar} and {Th. Kropf}},
  title     ={Accelerating Tableaux Proofs using Compact Representations},
  journal   ={Journal of Formal Methods in System Design},
  year      ={1993},
  key       ={ScKK93b},
}
@proceedings{HOL92,
  title       ={International Workshop on Higher Order Logic Theorem
                Proving and its Applications},
  year        ={1992},
  editor      ={{L. Claesen} and {M. Gordon}},
  publisher   ={Elsevier Science Publishers},
  organization={IFIP TC10/WG10.2},
  address     ={Leuven, Belgium},
  month       ={September},
  note        ={},
  key         ={HOL92},
}
-- 
Thomas Kropf, Institut fuer Rechnerentwurf und Fehlertoleranz,
Universitaet Karlsruhe, P.O. Box 6980, D-76128 Karlsruhe, Germany
email: kropf@ira.uka.de     Tel.: +49 721 608 4220    FAX: +49 721 370 455