Reasoning About Order Crossover in Genetic Algorithms.

The formal modeling and verification of algorithms is a challenging task, but it is a necessary requirement for the proof of correctness. Evolutionary computation and theorem proving approach of formal methods are two different domains in theoretical computer science. Using Prototype Verification System (PVS), this paper presents a method of formal specification, reasoning and verification for order crossover operator in Genetic Algorithms (GAs) and their rudimentary properties. Order crossover operator is first formally specified in PVS specification language. Some other operators used in the definitions of order crossover are also specified. PVS theorem prover is then used to prove some properties of order crossover and operators.