Résolution d'exercices via Equinox/Paradox :

Automated theorem prover & finite-domain model finder for pure first-order logic with equality.

---

Ressources :

• Equinox and Paradox website
• paradox_2010_01_28_with_script.tar.gz
    (Archive contenant la version 2008-08-25 de Paradox/Equinox
     , un patch afin de permettre la compilation avec GCC 4.4.2 et GHC 6.10.4 et supprimer des erreurs de segmentation
     et un script pour faciliter et automatiser son utilisation.)

---

Pré-requis :

• 1. Installation :
  
  Compiler les sources via make
  et ajouter éventuellement le dossier contenant les exécutables paradox, equinox et logic au $PATH.
  
  
• 2. Syntaxe (tptp syntax) :
  
  
  
  Remarque : Les prédicats, les fonctions et les constantes commencent par une minuscule et les variables par une majuscule !!!
  
  
• 3. Script :
  
  Le script "logic" a été créé afin de faciliter l'utilisation du programme.
  
  3 modes existent pour l'instant :
  
    -sat (Pour tester la consistance d'une formule)
    -csq (Pour tester une règle d'inférence)
    -cmp (Pour comparer des formules)
  
  Se référer aux différents exemples et au fichier README pour l'utilisation du script !

---

Exemples :

• Exemple 1 :
  
  
  
  logic -sat ex1 > ex1_res
  
    -> ex1, ex1_res
  
  
• Exemple 2 :
  
  
  
  logic -sat ex2 > ex2_res
  
    -> ex2, ex2_res
  
  
• Exemple 3 :
  
  
  
  logic -cmp ex3 > ex3_res
  
    -> ex3, ex3_res
  
  
• Exemple 4 :
  
  
  
  logic -cmp ex4 > ex4_res
  
    -> ex4, ex4_res
  
  
• Exemple 5 :
  
  
  
  logic -cmp ex5 > ex5_res
  
    -> ex5, ex5_res
  
  
• Exemple 6 :
  
  
  
  logic -csq ex6 > ex6_res
  
    -> ex6, ex6_res
  
  
• Exemple 7 :
  
  Someone who lives in Dreadbury Mansion killed Aunt Agatha.
  Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live therein.
  A killer always hates his victim, and is never richer than his victim.
  Charles hates no one that Aunt Agatha hates.
  Agatha hates everyone except the butler.
  The butler hates everyone not richer than Aunt Agatha.
  The butler hates everyone Aunt Agatha hates.
  No one hates everyone.
  Agatha is not the butler.
  
  Therefore : Agatha killed herself.
  
  logic -csq agatha > agatha_res
  
    -> agatha, agatha_res
  
  

  <-- Retour à la page du cours