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
of Automated Reasoning, volume 47(1), June 2011, pages
© 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.