Hi,
I'm trying to understand HOL Light. The forward reasoning subsystem seems
quite simple and lovely, but I'm confused by the backward reasoning. In
particular, the source file tactics.ml opens with the key definition:
type goal = (string * thm) list * term
How does it make sense that the hypotheses are *theorems*? I would have
expected them to be terms, since generally speaking a hypothesis is not
something that has already been proved.
When I saw that there is a function "set_goal" that does take a list of
terms (by simply mapping each term t to the theorem t |- t), and also that
the function "print_goal" only prints the *conclusion* of each hypothesis,
my guess was that the hypotheses are simply encoded as theorems of the form
t |- t for some unknown technical reason. However, a quick hack revealed
that at least internally, HOL Light uses hypotheses that are not of this
form.
Thanks for your help,
Jeremy
------------------------------------------------------------------------------
Create and Deploy Rich Internet Apps outside the browser with Adobe(R)AIR(TM)
software. With Adobe AIR, Ajax developers can use existing skills and code to
build responsive, highly engaging applications that combine the power of local
resources and data with the reach of the web. Download the Adobe AIR SDK and
Ajax docs to start building applications today-http://p.sf.net/sfu/adobe-com
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
