Integrating A First-order Automatic prover In The HOL Environment
Rakesh Kumar, Thomas Kröpf, Klaus Schneider · 2005
this paper it is shown how it is possible to automate these tasks by integrating a first-order automated theorem proving tool, called FAUST, into HOL. It is based on an efficient variant of the well-known sequent calculus. In order to maintain the high confidence in HOL-generated proofs, FAUST is able to generate HOL tactics which may be used to post-justify the theorems derived by FAUST in HOL. The underlying calculus of FAUST, the tactic generation, as well as experimental results are presented. 1. INTRODUCTION Although HOL is a very powerful tool for proving various formulae in higher-order logic, it is primarily interactive. In using HOL for hardware verification, we have found that one very often comes across first-order or simple higherorder formulae whose correctness is easy but tedious to prove. Since our main motivation is to build a hardware verification tool based on HOL, which can be used by normal circuit designers with little knowledge in theorem proving, we were keen on automating as much as possible.