Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator

Authors

  • Concepción Vidal
  • Felicidad Aguado
  • José Luis Doncel
  • Jose María Molinelli
  • Gilberto Perez

DOI:

https://doi.org/10.6092/issn.1972-5787/1052

Abstract

In this article we present the implementation and formal verification, using the Coq system, of a generalized version of the crossover operator applied to genetic algorithms (GA). The first part of this work defines the multiple crossover of two lists in any finite number of points, generalizing a previous definition by Uchibori. In the second part, we show that the definition does not depend on the order of the list of points. Then, a more efficient definition of the crossover operation is provided, and formally proved to be equivalent to the previous one, exploiting the notion of difference list.

Downloads

Published

2008-10-14

How to Cite

Vidal, C., Aguado, F., Doncel, J. L., Molinelli, J. M., & Perez, G. (2008). Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator. Journal of Formalized Reasoning, 1(1), 25–37. https://doi.org/10.6092/issn.1972-5787/1052

Issue

Section

Articles