Advertisement

Certified Genetic Algorithms: Crossover Operators for Permutations

  • F. Aguado
  • J. L. Doncel
  • J. M. Molinelli
  • G. Pérez
  • C. Vidal
  • A. Vieites
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4739)

Abstract

In the context of Genetic Algorithms, the use of permutations for representing the chromosomes, instead of the most common binary encoding, has turned out to be more natural and convenient in order to resolve some optimization problems. With the purpose of adapting the classical crossover to this special representation, several proposals can be found in the literature [2,3,8]. In this paper we use Coq to formally implement some of these crossover operators and also to verify that they satisfy the required specifications. As we have considered permutations of (possibly) repeated elements, we can cover a wider collection of applications.

Keywords

Genetic Algorithm Crossover Coq Calculus of Inductive Constructions Specification Theorem Proving 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aguado, F., Doncel, J.L., Molinelli, J.M., Pérez, G., Vidal, C.: Genetic Algorithms in Coq. Generalization and Formalization of the Crossover Operator. Theoretical Computer Science (2006) (sumited)Google Scholar
  2. 2.
    Davis, L.: Applying Adaptive Algorithms to Epistatic Domains. In: IJCAI85, Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pp. 162–164 (1985)Google Scholar
  3. 3.
    Davis, L.: Handbook of Genetic Algorithms, Van Nostrand Reinhold, New York (1991)Google Scholar
  4. 4.
    Holland, J.H.: Adaptation in Natural and Artificial Systems, University of Michigan Press, Ann Arbor (1975)Google Scholar
  5. 5.
    De Jong, A.K.: An Analysis of the Behavior of a class of Genetic Adaptive Systems, PhD Thesis, University of Michigan (1975)Google Scholar
  6. 6.
    Mitchell, M.: An introduction to Genetic Algoritms. MIT Press, Massachusetts (1996)Google Scholar
  7. 7.
    Paulin-Mhoring, C.: Extraction de programmes dans le calcul des constructions, Thése de doctorat, Université de Paris VII (1989)Google Scholar
  8. 8.
    Syswerda, G.: Schedule Optimization using Genetic Algorithms. In: [3], ch. 21, pp. 332–349Google Scholar
  9. 9.
    INRIA. The Coq proof assistant, http://coq.inria.fr

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • F. Aguado
    • 1
  • J. L. Doncel
    • 1
  • J. M. Molinelli
    • 1
  • G. Pérez
    • 1
  • C. Vidal
    • 1
  • A. Vieites
    • 1
  1. 1.Departament of Computer Science, University of A Coruña, A CoruñaSpain

Personalised recommendations