| dbo:abstract
|
- En la Demostración automática de teoremas, PhoX es un asistenete de pruebas que es eXtensible. El usuario le da a PhoX un objetivo inicial, guiándole a través de los subobjetivos y pruebas, para llegar al objetivo final. Internamente, PhoX construye árboles de deducción naturales. Cada fórmula probada con anterioridad puede convertirse en una regla futura para grandes generaciones PhoX fue originalmente diseñado e implementado por en el lenguaje de programación . Él ha continuando guiando el desarrollo actual, fruto de una colaboración entre la y la .
* Datos: Q603143 (es)
- 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)
- In automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees. Each previously proven formula can become a rule for later proofs. PhoX was originally designed and implemented by in the OCaml programming language. He has continued to lead the current development team, a joint effort of University of Savoy and University Paris VII. The primary aim of the PhoX project creating a user friendly proof checker using the type system developed by at University Paris VII. It is meant to be more intuitive than other systems while remaining extensible, efficient, and expressive. Compared to other systems, the proof-building syntax is simplified and closer to natural language. Other features include GUI-driven proof construction, rendering formatted output, and proof of correctness of programs in the ML programming language. PhoX is currently used to teach logic at Savoy University. It is in an experimental but usable state. It is released under CeCILL 2.0. (en)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 1454 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- En la Demostración automática de teoremas, PhoX es un asistenete de pruebas que es eXtensible. El usuario le da a PhoX un objetivo inicial, guiándole a través de los subobjetivos y pruebas, para llegar al objetivo final. Internamente, PhoX construye árboles de deducción naturales. Cada fórmula probada con anterioridad puede convertirse en una regla futura para grandes generaciones PhoX fue originalmente diseñado e implementado por en el lenguaje de programación . Él ha continuando guiando el desarrollo actual, fruto de una colaboración entre la y la .
* Datos: Q603143 (es)
- In automated theorem proving, PhoX is a proof assistant based on higher-order logic which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees. Each previously proven formula can become a rule for later proofs. PhoX was originally designed and implemented by in the OCaml programming language. He has continued to lead the current development team, a joint effort of University of Savoy and University Paris VII. (en)
- 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 (es)
- PhoX (logiciel) (fr)
- PhoX (en)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |