
Ce rpertoire contient des exemples pour vous permettre 
d'apprendre le logiciel.

Chaque exemple comprends un fichier " trou" nommer xxx_quest.phx, a
qui contient des indications pour complter les trous et un corrig 
xxx_cor.phx.

Ces exemples couvrent des points prcis que voici:


- tautologie_quest.phx

  Le but de cet exemple est double: 
  - on introduit progressivement les commandes les plus simples du
    systme PhoX sur des exemples simples de logique propositionnelle ou
    du calcul des prdicats. 
  - Ces exemples peuvent aussi servir d'illustration pour pour une introduction
     la logique auprs des tudiants. 

- intro_quest.phx

  Le but de ce fichier est galement d'introduire aux principales
  commandes de preuve de PhoX  travers des rsultats trs lmentaires
  sur les ordres (quivalence entre les axiomatisation d'ordre strict et
  d'ordre large).

- intro2_quest.phx

  La suite du prcdent : les commandes de preuves concernant
  l'existentielle -- l'oprateur de description dfinie (approche trs
  partielle)

- sort_quest.phx
  
  Couvre une utilisation assez avanc du logiciel avec les 
  commanded new_intro, new_elim et new_rewrite qui permettent 
  d'tendre et de controler les tactiques de preuves (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. 

