PhoX (logiciel)
- PhoX (logiciel)
-
PhoX (1994) est un assistant de preuve développé par Christophe Raffalli à l'Université de Savoie et antérieurement à Jussieu avec la participation de Philippe Curmin, Pascal Manoury et Paul Roziere.
Son nom provient du fait qu'un renard (en anglais fox) peut manger un coq (Coq est un autre assistant de preuve). Il signifie également Proof assistant in Higher Order logic eXtensible.
Il a été écrit dans le langage Objective Caml, et peut être utilisé sur la plus grande partie des systèmes informatiques comme Linux, Windows et Mac OS X.
Ainsi que l'indique son nom en anglais, PhoX est basé sur la Logique d'ordre supérieur et est extensible. Un des principes de ce programme est d'être le plus convivial possible, et de demander peu de temps d'apprentissage, celui-ci étant utilisé pour l'enseignement auprès des étudiants de mathématiques.
Voici les différentes caractéristiques de PhoX :
- Les preuves sont développées en déduction naturelle.
- Un démonstrateur automatique modeste permet de terminer automatiquement les points de preuve aisés.
- Un raisonnement équationnel est également disponible, soit automatiquement, soit pour faire de la réécriture.
- Les règles peuvent être étendues par l'utilisateur, tout comme la syntaxe.
- L'arbre de preuve est construit au fur et à mesure de la preuve, et vérifié à la fin.
- Il est possible d'utiliser des modules, dans une mesure qui ne permet pas la quantification universelle sur ceux-ci.
Voir aussi
PML
Liens et documents externes
- (en) Le site du projet
- Christophe Raffalli travaille actuellement sur un autre assistant de démonstration, PML (Proved ML ou Programmable Mathematical Logic) Site de PML
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article PhoX (logiciel) de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
PhoX — (logiciel) PhoX (1994) est un assistant de preuve développé par Christophe Raffalli à l Université de Savoie et antérieurement à Jussieu avec la participation de Philippe Curmin, Pascal Manoury et Paul Roziere. Son nom provient du fait qu un… … Wikipédia en Français
Phox — (logiciel) PhoX (1994) est un assistant de preuve développé par Christophe Raffalli à l Université de Savoie et antérieurement à Jussieu avec la participation de Philippe Curmin, Pascal Manoury et Paul Roziere. Son nom provient du fait qu un… … Wikipédia en Français
Projet:Mathématiques/Liste des articles de mathématiques — Cette page n est plus mise à jour depuis l arrêt de DumZiBoT. Pour demander sa remise en service, faire une requête sur WP:RBOT Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou… … Wikipédia en Français
Liste des articles de mathematiques — Projet:Mathématiques/Liste des articles de mathématiques Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou probabilités et statistiques via l un des trois bandeaux suivants … Wikipédia en Français
Assistant de preuve — En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des… … Wikipédia en Français
Assistant De Preuve — En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des… … Wikipédia en Français
Démonstrateur interactif de théorèmes — Assistant de preuve En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant l écriture et la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques … Wikipédia en Français
