Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <02740-0@swan.cl.cam.ac.uk>; Tue, 7 Apr 1992 09:09:34 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10369; Mon, 6 Apr 92 23:54:08 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA10360; Mon, 6 Apr 92 23:53:53 -0700 Message-Id: <9204070653.AA10360@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <16903-0@iraun1.ira.uka.de>; Tue, 7 Apr 1992 08:53:49 +0000 To: markaa@edu.cornell.ee.ultrastar Subject: Re: interfacing thm provers and other circuit "verifiers" In-Reply-To: Mail from '"Mark D. Aagaard" ' dated: Mon, 6 Apr 92 17:51:34 -0400 Cc: info-hol@edu.uidaho.cs.ted Date: Tue, 7 Apr 92 8:51:30 MET DST From: kumar@de.uka.ira We have been looking into similar aspects for the past year now. We have implemented a first-order theorem prover within HOL, which is capable of solving the goals which result out of a hardware proving environment in HOL called MEPHISTO. The goal to be proved is broken down semi-automatically into a set of subgoals and the rest is taken care of by FAUST, the first-order prover. The prover is an ML function, and in the production mode produces proofs, which are not HOL proofs. However, in the batch mode an automatic tactic is created which solves the goal within HOL. The other work that I know of is the work being done by Joyce (joyce@cs.ubc.ca) and Seeger at UBC Vancouver. They have combined the Cosmos (Switch level simulator) and HOL. A list of our publications are given below: Cheers, Kumar ***************************************************************************************** [ScKK 91a] "Automating Most Parts of Hardware Proofs in HOL", Proc. CAV-91, to appear as LNCS, Springer Verlag. [ScKK 91b] "Structuring Hardware Proofs: First Steps towards Automation in a Higher-Order Environment, Proc. of VLSI 91, A. Halaas and P.B.Denyer, IFIP Transactions A-1, Elsevier Publishers, North-Holland, 1991, pp. 81-90. [KKSc 91a] "Integrating a First-Order Automatic Prover in the HOL Environment", Proc. International Workshop on HOL Theorem Proving System and its Applications, Davis, California, Aug. 1991. [KKSc 91b] "First Steps towards Automating Hardware Proofs in HOL", Proc. International Workshop on HOL Theorem Proving System and its Applications, Davis, California, Aug. 1991. ******************************************************************************* Ramayya Kumar | email: kumar@ira.uka.de Institut fuer Rechnerentwurf und Fehlertoleranz, | Tel.: +49 (721) 608 4354 Fakultaet fuer Informatik, Universitaet Karlsruhe,| Fax: +49 (721) 370455 P.O. Box 6980, W-7500 Karlsruhe 1, | Germany |