文章基本信息

标题：Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator
本地全文：下载
作者：Concepción Vidal ; Felicidad Aguado ; José Luis Doncel 等
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2008
卷号：1
期号：1
页码：25-37
DOI：10.6092/issn.1972-5787/1052
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：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.