| Version | Source | Windows | Linux | Raspberry Pi | Documentation | Features | Fonctionnalités |
| v1 | pl-v1.hs | English | Initial version in Haskell | Version initiale en Haskell | |||
| v2 | pl-v2.hs pli.c | pli-linux | pli-rpi | English |
Initial C version Right transymmetry |
Version initiale en C Transymétrie droite |
|
| v3 | pl.c | pl-v3.exe | pl-linux | pl-rpi |
English
Français Tutorial |
Extensions : / : reduction step left \ : reduction step right ? : display |
Extensions : / : étape de réduction à gauche \ : étape de réduction à droite ? : afficher |
| v4 | pl-gtr.c | pl-gtr.exe | pl-gtr-linux | pl-gtr-rpi |
English
Français Tutorial |
Generalized transitivity with reduction | Transitivité généralisée avec réduction |
| v5 | pl-new.c | pl-new.exe | pl-new-linux | pl-new-rpi |
English
Français Tutorial |
New syntax for transitivity : x ; y | Nouvelle syntaxe pour la transitivité : x ; y |
| v6 | pl-new-clean.c | pl-new-clean.exe | pl-new-clean-linux | pl-new-clean-rpi | Obsolete features removed | Fonctionnalités obsolètes supprimées | |
| v7 | fpl.c | fpl.exe | fpl-linux | fpl-rpi | English | Fuzzy logic | Logique floue |
| v8 | pl-v8.c | pl-v8.exe | pl-v8-linux | pl-v8-rpi | Tutorial |
New operators Several proofs in one file Named proofs : & name proof |
Nouveaux opérateurs Plusieurs démonstrations dans un fichier Démonstrations nommées : & nom démonstration |
| v9 | pl-v9.c | pl-v9.exe | pl-v9-linux | pl-v9-rpi |
Check if another proof already has this name before naming a proof Print full definition of a proof with + Load file with "file" Echo when read from file and print reduction of proof ^x (f x) = f ~x reduces x at reading Allow prefixed operators in symbols (not at beginning) Constructor `x (RFE) : a = b |- (a = b) = (a = b) reduce [a *] -> a option -Q : read file without echo option -r : print reduction of proofs read from file |
Vérifier si une autre démonstration a déjà ce nom avant de nommer une démonstration Afficher la définition complète d'une démonstration avec + Charger un fichier avec "fichier" Echo lecture fichier et affichage réduction démonstration ^x (f x) = f ~x réduit x à la lecture Autoriser les caractères des opérateurs préfixés dans les symboles (pas au début) Constructeur `x (RFE) : a = b |- (a = b) = (a = b) reduce [a *] -> a option -Q : lecture fichier sans écho option -r : afficher la réduction des démonstrations lues dans un fichier |
|
| v10 | pl-v10.c | pl-v10.exe | pl-v10-linux | pl-v10-rpi |
Introduced '_' which represents unknowns like Prolog variables and can be instantiated with any value Display recursive proofs Option -o for occur-check `x (RFE) removed `x : search for matching proof for transitivity Circular proofs Option -f : full reduction Option -u : Display only value of unknown (_) if it has a value and do not display instantiations of unknowns |
Introduction de '_' qui représente des inconnues comme les variables en Prolog et peut être instancié par une valeur quelconque Affichage des démonstrations récursives Option -o pour test d'occurence `x (RFE) supprimé `x : cherche une démonstration compatible pour transitivité Démonstrations circulaires Option -f : réduction complète Option -u : Afficher uniquement la valeur de l'inconnue (_) si elle a une valeur et ne pas afficher les instantiations des inconnues |
|
| v11 |
Windows 64 bits : pl-v11_w64.c schedule_w64.h schedule_w64.c Linux : pl-v11.c schedule.h schedule.c |
pl-v11.exe | pl-v11-linux | pl-v11-rpi | English |
Option -a : use coroutines Option -g : GTR (;) with alt Option -U : unknown (_) with alt |
Option -a : utiliser les coroutines Option -g : GTR (;) avec alt Option -U : inconnue (_) avec alt |
| v12 |
Windows 64 bits : pl-v12_w64.c schedule_w64.h schedule_w64.c Linux : pl-v12.c schedule.h schedule.c |
pl-v12.exe | pl-v12-linux | pl-v12-rpi | English |
Deprecated operator "-" for application removed New operator "-" for full reduction of right part of conclusion introduced Option -h : display help Option -R : elementary reduction may reduce both subproofs of a proof |
Opérateur obsolète "-" pour l'application supprimé Nouvel opérateur "-" pour réduction complète de la partie droite de la conclusion introduit Option -h : afficher de l'aide Option -R : une réduction élémentaire peut réduire à la fois les deux sous-démonstrations d'une démonstration |