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
