<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Glen-</p>
<p>Sorry I didn't respond to this sooner... I had a hard time
"getting around to" exploring TheoremDep (and ConcepDag) enough to
comment (meaningfully?).</p>
<p>All I think Frank and Joe did was make a jump from TheoremDep the
tool to imagining things one might do with the underlying
ConcepDag data structure... "proof generation" I suppose.</p>
<p>I have my own "so what" homunculus. I have a BS in Math but
definitely recognized that I would never be a "Mathematician". I
appreciate the spirit and perspective of *real Mathematicians* and
(sometimes) even respect their contributions when they are driven
by curiosity or "because it is there" which sometimes anticipates
the practical needs of Engineering and Science. The old
fascination with why mathematics (as a pure abstraction) seems to
line up so well with physical reality comes up again. I think
there is some kind of anthropic principle involved? Do you have
any parallax on this?</p>
<p>I would *also* like to try to lay out the ConceptDAG data
structure with enough interactivity to do as you suggest ...
removing a node and seeing what "breaks"... or possibly adjusting
weights on the edges? I'm not clear there is a meaningful
semantic to that, but as usual I'm interested in trying to get a
"big picture". I did a project like this with the Gene Ontology
in 2004 or so...</p>
<p><img src="cid:part1.9864CA59.8B5068A7@swcp.com" alt=""></p>
<div class="moz-cite-prefix">The Gene Ontology is a partially
ordered set which provided more constraints (and opportunities)...
in this example, we didn't delete individual nodes, but could
adjust the force-directed layout paramaters as well as grab any
node and drag it far from it's equilibrium position. This was
useful for untangling local energy minima but also for inferring
dependencies.<br>
</div>
<p>- Steve<br>
</p>
</body>
</html>