INRIA Sophia Antipolis

The CtCoq User Interface

              INRIA Sophia Antipolis


         distribution CtCoq 



This page in English


CtCoq est maintenant remplacé par pcoq.

Ce qu'est CtCoq

CtCoq fournit un environnement de travail pour le système de preuve Coq. Cet environnement a été développé en utilisant une méthode générale pour la construction d'interfaces homme-machine pour les systèmes de preuve. Il a les caractèristiques suivantes:
une interface graphique:
les formules et les commandes sont affichées en utilisant des polices de caractères et des couleurs multiples:
des mécanismes d'édition et de présentation structurés:
L'environnement fournit les moyens d'éditer structurellement formules et commandes, des sous-expressions entières peuvent e^tre réduite en un seule geste avec la souris et de nouvelles notations peuvent e^tre ajoutées aisément.
une edition dirigée par des menus:
L'environnement fournit des menus pour construire de nouvelles commandes et formules. Ces menus sont facilement extensible.
la preuve par sélection:
L'environment utilise la structure des formules logiques pour aider systématiquement l'utilisateur àguider la preuve par de simple sélection à la souris.
l'explication textuelle des preuves:
En utilisant ses puissantes possibilités d'affichages, l'environnement CtCoq peut présenter les termes de preuves d'une façon qui s'approche du langage naturel.
séparation entre l'interface et le système de preuve:
L'interface graphique et le système de preuve tournent comme deux processus indépendants.

Pour en savoir plus sur CtCoq, vous pouvez aussi jeter un coup d'oeil à la documentation en ligne (en anglais).

Comment obtenir CtCoq

L'interface marche avec la version 6.2.3 de Coq. Si vous voulez voir quelques articles ou la documentation, cliquez ici.
Pour plus d'informations, envoyez un courrier à ctcoq-request@sophia.inria.fr

Information général

CtCoq est basé sur un travail d'environnement de programmation, Centaur, qui est developpé dans le projet CROAP à INRIA Sophia Antipolis.
Yves Bertot / INRIA Sophia Antipolis / Yves.Bertot@inria.fr