Other sources of documentation

• The web page of :

  http://www.lama.univ-savoie.fr/~raffalli/phox.html

• The documentation of the library (file doc/libdoc.dvi). You can also look at the PhoX files in the lib directory

• An article relating a teaching experiment with PhoX [5]. This article gives a short presentation of PhoX giving one commented example and an appendix of the main commands. It is also a good introduction to PhoX.

  It is available from the Internet in french and english:

  ftp://www.lama.univ-savoie.fr/pub/users/RAFFALLI/Papers/arao-fr.ps.gzftp://www.lama.univ-savoie.fr/pub/users/RAFFALLI/Papers/arao-en.ps.gz

• The folder tutorial/french : it contains tutorial. It is only in french. Each tutorial comes with two files: xxx_quest.phx and xxx_cor.phx. In the first one there are questions: ``dots'' that you need to replace by the proper sequence of commands. The second one contains valid answer to all the questions.

  There are three kinds of tutorials (see the ``README'' in tutorial/french for a more detailed description):

  • Tutorial intended to learn PhoX itself: tautologie_quest.phx, intro_quest.phx and sort_quest.phx.
  • Tutorial intended to learn standard mathematics: ideal_quest.phx, commutation_quest.phx, topo_quest.phx, analyse_quest.phx and group_quest.phx.
  • Tutorial intended to learn Elogic: tautologie_quest.phx and minlog_quest.phx (the latest tutorial is difficult).

  We plan to translate these tutorials to english.

• The folder examples and examples/mini of the distribution : they contain a lot of examples of proof development. Beware that a lot of these examples were develop for some older version of PhoX and could be improved using recent features.