Hi Mario,
Yes, as Freek says, Tactician would do the sort of thing you need, but
is only for HOL Light. It works on the vast majority of tactic proofs
as they are typically written in HOL Light, say perhaps 1 in every 1,000
proof script lines might trip it up. It could be ported to HOL4, but
this would not be easy to get working as well as it does for HOL Light,
because it plays about with the innards of OCaml and equivalent tweaking
of PolyML would be required.
Mark.
On 07/08/2020 10:02, Freek Wiedijk wrote:
Dear Mario,
Hello. In HOL4 is there a way to generate something like the entries
in
Metamath proof explorer for the subgoals generated within a proof and
the tactics used to solve them? Example:
<http://us.metamath.org/mpeuni/eluniab.html>
For HOL Light there is Mark Adams's "tactician" which
I expect would make something like this possible (even
though I expect it only would work on the majority of
proofs, and not be guaranteed to work on all of them).
But that's HOL Light, not HOL4.
Freek
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
