PhoX

PhoX

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 Christophe Raffalli in the Ocaml programming language. He has continued to lead the current development team, a joint effort of Savoy University and .

The primary aim of the PhoX project creating a user friendly proof checker using the type system developed by Jean-Louis Krivine 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.

External links

* [http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html PhoX Website]


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • PhoX — Saltar a navegación, búsqueda 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 de los subobjetivos y pruebas, para llegar al objetivo …   Wikipedia Español

  • 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

  • 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… …   Wikipédia en Français

  • phox — (= phox47; phox67) Components of the NADPH oxidase system in phagocytes, the system responsible for generating an oxidative burst and thus bacterial killing. Phox47 and phox67 are cytoplasmic and only associate with the integral membrane… …   Dictionary of molecular biology

  • PHOX — Photonics Corporation (Business » NASDAQ Symbols) …   Abbreviations dictionary

  • PHOX — paired mesoderm homeobox [gene] …   Medical dictionary

  • phox — o (G). Pointed …   Dictionary of word roots and combining forms

  • PHOX — abbr. PHOTONICS CORP NASDAQ …   Dictionary of abbreviations

  • PHOX — • paired mesoderm homeobox [gene] …   Dictionary of medical acronyms & abbreviations

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”