Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de
Subject: hol90 should have more control about proofs
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Thu, 08 Feb 1996 08:47:43 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.606:08.02.96.07.48.41"@ira.uka.de>

First, thank's a lot for all how responded on the constant/definition subject.
Here is another thing falling in the same category:

Given a theorem of a theory, there is currently no "direct" way to
COMPUTE the dependencies of this theorem to other theorems, i.e. the
proof of this theorem is not stored in any way and thus the hol system
does not know, which theorems where needed to prove this theorem. HOL90
in its current philosophy is imho not in a good situation to store the
proofs of a theorem in the theory, too, simply because the proof could
be any "strange/fuzzy/hacked" sml-function (of a certain type, at least).

A good system for having much better control over proofs, especially for
storing proofs and analyzing their dependencies (that imho makes a
hol-system much more user-friendly!) should have a more complex notion of 
tactics/rules in order to e.g. store them space/time--efficiently
and to store dependencies space/time--efficiently. This would also
require a much more rigorous mechanism for introducing new tactics/rules
instead of the very openness philosophy of HOL90.

I think there already was a discussion about that on the last HOL-workshop.
However, considering writing sml-functions for printing out dependencies
as graphs using the graph-visualization system daVinci, I again ran into
that problem, making these questions and comments here. Personally, I think
HOL90 should go the way of having much better control over proofs. What
are other HOL90-Users thinking about that??

Ralf


(*********************************************************************)
(*                                                                   *)
(*  Ralf Reetz                                                       *)
(*  Research Assistent                                               *)
(*  Sonderforschungsbereich 358 der deutschen Forschungsgemeinschaft *)
(*  "Automatisierter Systementwurf"                                  *)
(*  University of Karlsruhe                                          *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                  *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany                *)
(*                                                                   *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de    *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html         *)
(*  fax:    +49 721 370455                                           *)
(*  tel:    +49 721 6084220                                          *)
(*                                                                   *)
(*********************************************************************)