1. Overview
  2. Docs



The folder constains examples to learn how to use PhoX.

Each example uses a file with "holes" to fill named xxx_quest.phx, and
a complete file named xxx_cor.phx.

These examples cover some precise points:

- tautologie_quest.phx

  The goal of this example is two sided:
  - We progressively introduce the simplest commands of PhoX on simple
    formulas of prositional logic or predicate calculus.
  - These examples can also be used as an introduction in logic for students.

- sort_quest.phx
  Covers a relatively advanced use of the software using the new_intro, 
  new_elim and new_rewrite commands which allow to change the behavior and
  the proof tactics (intro, elim, left, trivial, ...)

- Exo de math (fichiers ideal_quest.phx,
               commutation_quest.phx, topo_quest.phx,
               analyse_quest.phx et group_quest.phx)

  Des exercices pour apprendre les math en utilisant PhoX (on apprend
  PhoX en mme temps, mais le but rel est d'apprendre des maths !)
- Logique Minimale (fichier minlog_quest.phx )

  But similaire au prcdent, mais le sujet s'adresse plus  un logicien
  de bon niveau.