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.
