Pcoq fournit un environnement de travail pour le système de preuve Coq. Il a été développé en suivant une approche générale pour la construction d'interfaces utilisateurs pour ces systèmes. Il réunit les caractéristiques suivantes:
- Interface graphique:
- des polices de caractères multiples et des couleurs sont utilisées pour afficher les formules mathématiques et les commandes.
- séparation entre l'interface and le système de preuve:
- L'interface graphique et Coq sont deux processus indépendants. Les utilisateurs peuve choisir de faire tourner l'un des processus sur une autre machine accessible sur le réseau.
- Des mécanismes d'édition et de présentation structurés:
- L'environnement fournit des moyens pour éditer les formules en respectant leur structure. De nouvelles notations peuvent être ajoutées facilement,
- proof by pointing:
- L'environnement utilise la structure des formules logique pour aider l'utilisateur à effectuer les étapes du raisonnement en les désignant à la souris.
- Utilise Java
- Pcoq bénéficie de la portabilité combinée Ocaml et Java.
Pcoq est construit et maintenu par l'équipe Lemme à
l'INRIA Sophia-Antipolis
. Ce groupe s'intéresse à de nombreux aspects de
l'utilisation du système coq. Par exemple, nous
collaborons également avec Xiao Gang de l'Université de
Nice pour rendre Coq accessible sur le Web, au travers de son
serveur de mathématiques interactives (suivre les liens
Dernières mises à jour de cette page
- 18 Janvier 2002. Distribution de Pcoq-1.3.
- 2 Mai 2001. Distribution de Pcoq-1.2.