Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 13 Feb 1995 11:49:15 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA27591;
          Mon, 13 Feb 1995 04:31:46 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA27581;
          Mon, 13 Feb 1995 04:31:25 -0700
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Mon, 13 Feb 1995 12:29:04 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <23315-0@i80fs2.ira.uka.de>;
          Mon, 13 Feb 1995 12:28:59 +0100
Date: Mon, 13 Feb 95 12:28:58 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu, Donald.Syme@cl.cam.ac.uk
Subject: visualization of parents for clarity
Message-Id: <"i80fs2.ira.317:13.02.95.11.28.59"@ira.uka.de>

Donald Syme writes:

>I'm not sure about this.  The best reason to directly add a
>parent which is already an ancestor is for clarity - i.e. to show that a
>theory uses another theory directly, and not merely as an artifact
>of it being an ancestor via a third theory.

I think that using a graph visualization system would be an elegant way
to make dependencies more clearly. That must not be constrained to parents
of a theory, think. e.g. of a dependence graphs for definitions/constants,
visualisation of the structure of terms, ...
E.g. , I myself have written a sml-function, which maps the term describing
attributed deriviation trees of my library "generator" to an input file for
the graph visualization system daVinci, so I just push the button an get
a graphical visualization of the attributation, which makes writing and
debugging attributation rules much easier.
So, what about a hol library, which contains various sml-functions for
converting serveral facts about the current theories in hol into daVinci-Graphs?
That makes dependencies more clearly, I think.

Ralf.

PS: for daVinci, see

http://www.informatik.uni-bremen.de/~inform/forschung/daVinci/daVinci.html

(**************************************************************)
(*                                                            *)
(*  Ralf Reetz                                                *)
(*                                                            *)
(*  University of Karlsruhe                                   *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz           *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany         *)
(*                                                            *)
(*  e-mail: reetz@ira.uka.de                                  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html  *)
(*                                                            *)
(**************************************************************)