The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4
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.
higher-order logic linear temporal logic theorem proving automated reasoning combining theorem provers model checking