TP Logique : Interpréteur logique
Pour ce TP nous nous passerons de Prolog, et allons implémenter un petit interpréteur logique directement en JAVA. suivez le guide.

Table des Matières

Introduction

Vous trouverez dans cette archive le squelette d'application. Il contient un lexer écrit en JFlex et un parser écrit en CUP. Souvenez-vous de vos TP d'AEL, vous pourrez examiner les fichiers .lex et .cup dans le répertoire spec si le sujet vous intéresse. Nous allons cependant nous concentrer sur le modèle sémantique. La grammaire des formules de ce langage est :
formule ::= formule2 "=>" formule1 (implication) | formule2 "<=>" formule1 (équivalence) | formule2 formule2 ::= formule3 "+" formule2 (ou) | formule3 "*" formule2 (et) | formule3 formule3 ::= "-"" formule3 | "(" formule1 ")" (parenthèses) | id (variable) | "T" (vrai) | "F" (faux)
Écrivez les classes
Et
,
Ou
,
Non
,
Implique
,
Equivalence
,
Constante
et
Variable
dans le répertoire
src/logicline/modeleSemantique/
. Pour le moment mettez un corps vide ou
return null;
pour les méthodes abstraites à implémenter. Les classes doivent donc hériter de la classe
Formule
et déclarer
package logicline.modeleSemantique
en début de fichier. Vous pouvez tenter un
make
et faire en sorte que le tout compile.
Le premier test consitera à afficher les formules propositionnelles. Pour cela il vous suffit d'implémenter la méthode
toString
dans les classes de chaque connecteur logique. En cadeau, voici des jolis caractères UTF-8 :
¬ ∨ ∧ ⇒ ⇔ T ⊥
. N'hésitez pas à afficher les parenthèses inutiles. On ne vous demande pas de faire une distinction des cas où elles sont utiles.
Vous pouvez maintenant tester votre programme avec la commande
./execSurFichierAnalyseurSyntaxique.sh test/formules
. Vous devriez obtenir ceci :
Exemple
./execSurFichierAnalyseurSyntaxique.sh test/formules (A) ∨ (¬(B)) ((a) ⇒ (b)) ⇒ (((b) ⇒ (c)) ⇒ ((a) ⇒ (c))) (¬((A) ∨ (B))) ⇔ ((¬(A)) ∧ (¬(B)))
Vous pouvez aussi utiliser l'interpréteur en ligne pour des tests rapides :
./execEnLigneAnalyseurSyntaxique.sh
. Validez votre phrase avec
Ctrl + D
deux fois.

Variables Libres

Nous aurons besoin par la suite de connaître les variables libres d'une formule. Nous représenterons un ensemble de variables libres par un
Set<String>
, que vous instancerez avec des
HashSet. Dans notre cas aucun connecteur ne lie de variable, donc toutes les variables sont libres.
Implémentez la méthode
variablesLibres
pour chaque type de formule. Pour les connecteurs ayant deux sous-formules, vous pouvez utiliser la méthode de la classe HashSet pour fusionner les deux ensembles.
Exemple
$ ./execSurFichierAnalyseurSyntaxique.sh test/vl A B b c a A B

Substitutions

Nous nous intéressons maintenant aux substitutions. Je vous rappelle qu'une substitution consiste à remplacer les occurrences libres de variables par des formules spécifiées. Je vous rappelle que dans notre cas toutes les variables sont libres. Les substitutions utiliseront la classe
Substitution
qui permet de gérer une liste de substitutions à travers deux méthodes :
  • public void set(String v, Formule f)
    qui permet de remplacer la variable
    v
    par la formule
    f
    .
  • public Formule get(String v)
    qui permet de récupérer la formule substituée à
    v
    .
Dans notre langage, les substitutions sont définies par la grammaire suivante :
substitution ::= "[" id "<=" formule1 listesub "]" listesub ::= "," id "<=" formule1 listesub |
Implémentez la méthode
substitue
qui va réaliser le substitution sur une formule.
Exemple
$ ./execSurFichierAnalyseurSyntaxique.sh test/substitution (A) ∨ (¬(⊤)) ((¬(b)) ⇒ ((d) ∨ (e))) ⇒ ((((d) ∨ (e)) ⇒ (c)) ⇒ ((¬(b)) ⇒ (c))) (¬(((C) ⇔ ((D) ⇒ (⊥))) ∨ (B))) ⇔ ((¬((C) ⇔ ((D) ⇒ (⊥)))) ∧ (¬(B)))

Forme Normale Conjonctive

Les FNC sont très utiles pour chercher les valuations qui satisfont des formules logiques. Rappelez-vous du cours, la mise en FNC consiste à
  • Supprimer les implications
  • Entrer les négations
  • Entrer les disjonctions
Implémentez la méthode
supprImplications
, qui va supprimer les implications et les équivalences grâce aux propriétés logiques suivantes :
  • A ⇒ B ≣ ¬A ∨ B
  • A ⇔ B ≣ (¬A ∨ B) ∧ (A ∨ ¬B)
Exemple
$ ./execEnLigneAnalyseurSyntaxique.sh Entrez le texte à analyser : fnc A => B. (¬(A)) ∨ (B)
Vous pouvez ignorer les exceptions pour le moment. Elles viennent du comportement par défaut des méthodes ci-dessous, implémentées dans la classe
Formule
.
Pour entrer les négations, nous devons savoir quel type de formule est sous la négation. Pour éviter d'utiliser la méthode
instanceof
, nous allons donc commencer par écrire une méthode
negation
qui retourne la négation d'une formule. Elle utilisera les propriétés suivantes pour faire quelques simplifications :
  • ¬¬A ≣ A
  • ¬(A ∨ B) ≣ ¬A ∧ ¬B
  • ¬(A ∧ B) ≣ ¬A ∨ ¬B
Exemple
Formule f = new Et(a,b); Formule f2 = f.negation(); System.out.println(f2); ((¬A) ∨ (¬B))
Écrivez maintenant la méthode
entrerNegations
qui va effectivement entrer les négations à l'intérieur de la formule.
Exemple
$ ./execEnLigneAnalyseurSyntaxique.sh Entrez le texte à analyser : fnc -(A + B). (¬(A)) ∧ (¬(B))
Entrer les disjonctions et sortir les conjonctions est un peu plus compliqué car nous travaillons sur deux sous-formules et deux types de connecteurs. Nous utiliserons la propriété suivante :
A ∨ (B ∧ C) ≣ (A ∨ B) ∧ (A ∨ C)
Écrivez la méthode
contientEt
qui retourne
true
si la formule contient un
Et
.
Nous allons maintenant examiner les cas possibles selon les sous-formules. Prenez une feuille de papier pour examiner les cas possibles. Implémentez ensuite les méthodes
ougauche
et
oudroite
qui retournent une formule qui remontent les
Et
en faisant descendre les
Ou
à gauche et à droite.
Vous pouvez maintenant implémenter la méthode
entrerDisjonctions
qui va utiliser les méthodes
contientEt
,
ougauche
et
oudroite
pour achever la transformation en FNC. Nous supposerons que les étapes précédentes de transformation en FNC sont effectuées, c'est-à-dire qu'il n'y a plus de'implications, ni d'équivalences, et que les non sont juste au dessus des variables.
Pour achever le travail, nous allons transformer une formule en FNC sous forme de liste de clauses. Plus tard nous les utiliserons pour trouver des valuations qui satisfont les formules. Pour le moment ça nous permet d'obtenir un affichage plus lisible des formules en FNC.
Implémentez la méthode
clauses
qui retourne une liste de clauses de type
ListeClauses
. La formule sur laquelle cette méthode est appelée est censée être en FNC. Si elle ne l'est pas, levez l'exception
NotFNCException
. En principe le travail est déjà fait dans la classe
Formule
. Si une clause est vraie (il suffit qu'un de ses littéraux le soit, ou qu'un littéral et sa négation soit dans la clause), on lèvera l'exception
TrueClauseException
. De même si une clause est fausse, on lèvera l'exception
FalseClauseException
. Ça nous permettra de faire quelques simplifications. De même vous pouvez utiliser l'exception
VariableClauseException
pour faire remonter la variable en sous-formule.

Table de vérité

Nous cherchons maintenant à afficher la table de vérité d'une formule. Pour cela nous devons évaluer la formule pour toute valuation de ses variables libres. Nous avons déjà écrit une méthode qui retourne les variables libres. Nous devons maintenant évaluer les formules, et générer toutes les valuations.
Implémentez la méthode
valeur
qui calcule la valeur d'une formule close. Cette méthode lève l'exception
VariableLibreException
si la formule contient une variable libre.
Nous pouvons maintenant afficher la table de vérité d'une formule en calculant toutes ses valuations possibles. Implémentez la méthode
tableVerite
, directement dans la classe
Formule
. Commencez par chercher la liste des variables libres. Construisez ensuite une liste de
Substitution
contenant toutes les valuations possibles. Chaque variable peut être soit la
Constante
⊤ soit la
Constante
⊥.
Exemple
$ ./execSurFichierAnalyseurSyntaxique.sh test/tableverite A |B |(A) ∨ (¬(B)) ⊥ |⊥ |⊤ ⊥ |⊤ |⊥ ⊤ |⊥ |⊤ ⊤ |⊤ |⊤ b |c |a |((a) ⇒ (b)) ⇒ (((b) ⇒ (c)) ⇒ ((a) ⇒ (c))) ⊥ |⊥ |⊥ |⊤ ⊤ |⊥ |⊥ |⊤ ⊥ |⊥ |⊤ |⊤ ⊤ |⊥ |⊤ |⊤ ⊥ |⊤ |⊥ |⊤ ⊤ |⊤ |⊥ |⊤ ⊥ |⊤ |⊤ |⊤ ⊤ |⊤ |⊤ |⊤ A |B |(¬((A) ∨ (B))) ⇔ ((¬(A)) ∧ (¬(B))) ⊥ |⊥ |⊤ ⊥ |⊤ |⊤ ⊤ |⊥ |⊤ ⊤ |⊤ |⊤

Davis-Puttnam

Notre aventure touche à sa fin. Il ne vous reste maintenant qu'à trouver une valuation qui satisfait votre formule. Pour celà nous utiliserons l'algorithme DPLL vu en cours. Je vous conseille de bien le relire et de le garder à porter de main. Nous travaillerons désormais sur des
ListeClauses
.
Implémentez la méthode
simplifieClause
de la classe
ListeClauses
, qui simplifie une liste de clauses dans laquelle on considère que le
litteral
donné vaut
valeur
. Elle lèvera donc une exception
NotSatisfiableException
si son littéral opposé forme une clause unitaire, supprimera les clauses contenant le littéral, et supprimera son opposé des autres clauses.
Implémentez la méthode dpll, qui va réaliser les 3 opérations phases de l'algorithme DPLL : À chaque opération, simplifiez, appelez
dpll
récursivement, puis ajoutez la substitution à celles de l'appel récursif. Lisez attentivement l'implémentation de la classe
clause
, elle contient des méthodes bien utiles.
Exemple
$ ./execSurFichierAnalyseurSyntaxique.sh test/dpll Formule en FNC : (a) ∨ (b) Liste de clauses : (b ∨ a) [b ← ⊤] Formule en FNC : ((a) ∨ (¬(b))) ∧ ((b) ∨ (c)) Liste de clauses : (¬b ∨ a) ∧ (b ∨ c) [a ← ⊤, b ← ⊤] Formule en FNC : (a) ∧ (((b) ∨ ((c) ∨ (¬(d)))) ∧ (((b) ∨ ((¬(c)) ∨ (e))) ∧ (((b) ∨ (¬(f))) ∧ (((d) ∨ (¬(e))) ∧ ((¬(d)) ∨ (¬(e))))))) Liste de clauses : (a) ∧ (¬d ∨ b ∨ c) ∧ (e ∨ b ∨ ¬c) ∧ (¬f ∨ b) ∧ (d ∨ ¬e) ∧ (¬d ∨ ¬e) [a ← ⊤, b ← ⊤, e ← ⊥]