You could use Joe Hurd's fork of HOL Light that adds support for recording
and exporting proofs in OpenTheory article format.
See http://gilith.com/research/opentheory/ and
http://src.gilith.com/hol-light.html.
On Sat, Oct 11, 2014 at 3:34 AM, Mario Carneiro <[email protected]> wrote:
> Hello,
>
> I'm interested in examining the core axiom functions of HOL so that I can
> produce diagnostic information on the actual proof process as the program
> runs. What is the best way to do this? I remember hearing somewhere that
> someone made a program to convert HOL light proofs into something
> understandable by an automated prover, and I am trying to something similar
> (I want to translate HOL proofs into another language), so I'm curious if
> there is an already established method for getting this sort of data out of
> the core.
>
> Mario Carneiro
>
>
> ------------------------------------------------------------------------------
> Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
> Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
> Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
> Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
> http://p.sf.net/sfu/Zoho
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
