Typed meta-interpretive learning for proof strategies
Colin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton, Alan Bundy · 2015
Abstract. Formal verification is increasingly used in industry. A pop-ular technique is interactive theorem proving, used for instance by Intel in HOL light. The ability to learn and re-apply proof strategies from a small set of proofs would significantly increase the productivity of these systems, and make them more cost-effective to use. Previous attempts have had limited success, which we believe is a result of missing key goal properties in the strategies. Capturing such properties will require pred-icate invention, and the only technique we are familiar which supports this is meta-interpretive learning (MIL). We show that MIL is applicable to this problem, but that it offers limited improvements over previous work. We then extend MIL with types and give preliminary results in-dicating that this extension learns better strategies with suitable goal properties. 1