Proof Searching in PVS Theorem Prover Using Simulated Annealing

The proof development process in PVS theorem prover is interactive in nature, that is not only laborious but consumes lots of time. For proof searching and optimization in PVS, a heuristic proof searching approach is provided where simulated annealing (SA) is used to search and optimize the proofs for formalized theorems/lemmas in PVS theories. In the proposed approach, random proof sequence is first generated from a population of frequently occurring PVS proof steps that are discovered with sequential pattern mining. Generated proof sequence then goes through the annealing process till its fitness matches with the fitness of the target proof sequence. Moreover, the performance of SA with a genetic algorithm (GA) is compared. Obtained results suggest that evolutionary/heuristic techniques can be combined with proof assistants to efficiently support proofs finding and optimization.