Proof Searching in HOL4 with Evolutionary and Heuristic Algorithms

Abstract

Theorem provers also known as mechanical reasoning systems are based on mathematical logics and are used in the modeling and analysis of sotware and hardware systems, particualrly safety-critical systems. Proof search ing and proof automation are the two most desired properties in interac tive theorem provers (ITPs) as they generally require manual user guidance, which can be quite cumbersome. In this thesis, we provide evolutionary and heuristic-based approaches (Genetic Algorithms (GAs) and Simulated Annealing (SA)) for proofs searching and optimization in various HOL4 the ories. In both approaches, random proof sequences are rst generated from a population of frequently occurring HOL4 proof steps that are discovered with sequential pattern mining. Generated proof sequences are then evolved with operators (crossover and mutation) in GA and with annealing process in SA, till their tness match the tness of the target proof sequences. For GA, various crossover and mutation operators are used to compare their ef fect on the overall performance of GAs in proof searching. Moreover, the performance of GA with SA is compared for various parameters. Obtained results suggest that integrating evolutionary and heuristic-based techniques with HOL4 allows us to e ciently support proof nding and optimization.