Hi Mario,
you might be interested in the "Proof Recording" mechanism. Look into the
subdirectory Proofrecording in HOL Light distribution. It has already been
employed for exporting theorems from HOL Light to Coq. Beside the README
in the above directory, you may find
other
information in the paper of Chantal Keller and Benjamin Werner
"
Importing HOL Light into Coq
".
Hope it can be useful,
Marco
2014-10-11 4:34 GMT+02:00 Mario Carneiro <di.g...@gmail.com>:
> 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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
