The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4

M. J. C. Gordon, M. Kaufmann, and S. Ray

Journal of Automated Reasoning, volume 47(1), June 2011, pages 1-16. Springer.

© 2010 Springer.


We present a case study illustrating how to exploit the expressive power of higher-order logic to complete a proof whose main lemma is already proved in a first-order theorem prover. Our proof exploits a link between the HOL4 and ACL2 proof systems to show correctness of a cone of influence reduction algorithm, implemented in ACL2, with respect to the classical semantics of linear temporal logic, formalized in HOL4.

Relevant files