Une implémentation de Zermelo Fraenkel en CoQ

G. ALEXANDRE

IBP-Litp 1996/05: Rapport de Recherche Litp / Litp research reports
37 pages - Février/February 1996 - French document.

PostScript : Ko /Kb

Titre / Title: Une implémentation de Zermelo Fraenkel en CoQ

Résumé : Nous présentons ici le codage de la théorie des ensembles de Zermelo - Fraenkel dans le prouveur CoQ, prouveur basé sue le Calcul des Constructions et la logique intuititionniste. Ce document constitue le manuel de référence du module MS et Basis.

Abstract : This paper presents an implementation of Zermelo-Fraenkel sets theory in the theorems prover CoQ. This prover used to deal with Calculus of Constructions and intuitionnistic logic. This document may be considered as the reference manual of the module MS et Basis.

Publications internes Litp 1996 / Litp research reports 1996