PhoX (1994) est un assistant de preuve développé par à l'Université de Savoie et antérieurement à Jussieu avec la participation de , et . 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 OCaml, et peut être utilisé sur la plus grande partie des systèmes informatiques comme Linux, Windows et Mac OS X. Voici les différentes caractéristiques de PhoX :

Property Value
dbo:abstract
  • PhoX (1994) est un assistant de preuve développé par à l'Université de Savoie et antérieurement à Jussieu avec la participation de , et . 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 OCaml, 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 : 1. * Les preuves sont développées en déduction naturelle. 2. * Un démonstrateur automatique modeste permet de terminer automatiquement les points de preuve aisés. 3. * Un raisonnement équationnel est également disponible, soit automatiquement, soit pour faire de la réécriture. 4. * Les règles peuvent être étendues par l'utilisateur, tout comme la syntaxe. 5. * L'arbre de preuve est construit au fur et à mesure de la preuve, et vérifié à la fin. 6. * Il est possible d'utiliser des modules, dans une mesure qui ne permet pas la quantification universelle sur ceux-ci. (fr)
  • PhoX (1994) est un assistant de preuve développé par à l'Université de Savoie et antérieurement à Jussieu avec la participation de , et . 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 OCaml, 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 : 1. * Les preuves sont développées en déduction naturelle. 2. * Un démonstrateur automatique modeste permet de terminer automatiquement les points de preuve aisés. 3. * Un raisonnement équationnel est également disponible, soit automatiquement, soit pour faire de la réécriture. 4. * Les règles peuvent être étendues par l'utilisateur, tout comme la syntaxe. 5. * L'arbre de preuve est construit au fur et à mesure de la preuve, et vérifié à la fin. 6. * Il est possible d'utiliser des modules, dans une mesure qui ne permet pas la quantification universelle sur ceux-ci. (fr)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 2614711 (xsd:integer)
dbo:wikiPageLength
  • 2161 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 168273866 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • PhoX (1994) est un assistant de preuve développé par à l'Université de Savoie et antérieurement à Jussieu avec la participation de , et . 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 OCaml, et peut être utilisé sur la plus grande partie des systèmes informatiques comme Linux, Windows et Mac OS X. Voici les différentes caractéristiques de PhoX : (fr)
  • PhoX (1994) est un assistant de preuve développé par à l'Université de Savoie et antérieurement à Jussieu avec la participation de , et . 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 OCaml, et peut être utilisé sur la plus grande partie des systèmes informatiques comme Linux, Windows et Mac OS X. Voici les différentes caractéristiques de PhoX : (fr)
rdfs:label
  • PhoX (logiciel) (fr)
  • PhoX (logiciel) (fr)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of