Simon Peyton-Jones <[EMAIL PROTECTED]> writes:
> What I have not done (any volunteers) is to export these rules, or
> the function definitions to a thm prover.
I am in the course of exporting function definitions
(and later probably also rules)
to the term graph transformation system HOPS
(
URL: http://www2.informatik.unibw-muenchen.de/kahl/HOPS/
)
which can also be considered as a fledgling theorem prover ---
anyway I expect the problems to be essentially the same.
I am trying to finish a short summary next week...
Wolfram
