An heuristic for axiomatic theories : the case of zermelo set theory

G. Alexandre, P. Maunoury

IBP-Litp 1996/15: Rapport de Recherche Litp / Litp research reports
15 pages - Mars/March 1996 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: An heuristic for axiomatic theories : the case of zermelo set theory

Résumé : Nous présentons dans cet article un algorithme améliorant le niveau d'automatisation des preuves dans les théories axiomatiques.Les principes initiaux de cet algorithme sont issus d'une implantation de la théorie des ensembles de Zermelo dans le prouveur CoQ, qui utilise la logique d'ordre supérieur. L'algorithme est conçu de façon à autoriser sa généralisation à d'autres théories axiomatiques comme la théorie naïve des ensembles, la théorie des groupes.

Abstract : We present in this paper an algorithm to increase the level of automatization of proofs of lemmas in axiomatic theories. The principles of the algorithm were suggested by the encoding of Zermelo set theory in the higher order framework of the CoQ proof assistant. The design of this algorithm is so that it can easily be generalized to further theories as naive set theory, group theory, and so on.

Publications internes Litp 1996 / Litp research reports 1996