Ce travail est dédié à l'implantation en Java de fonctionnalités liées au raisonnement en logique propositionnelle , il s'agit en particulier de pouvoir construire des formes normales conjonctives (CNF) et disjonctives (DNF) de formules propositionnelles et d'implanter un système de preuves par la méthode des tableaux.

1. Prérequis

Ce TP est la suite directe du TP 1: Syntaxe. Il est conseillé de reprendre le projet Java utilisé précédemment, cependant,  Il est possible de réaliser ce travail au sein d'un nouveau projet.

2. Sémantique

La sémantique de la logique propositionnelle décrit la façon d'interpréter une formule, c'est à dire la façon de lui donner une valeur.

2.4. Valeur d'une formule

La classe/interface Formula doit proposer une méthode public boolean value(Interpretation i) qui calcule la valeur de la formule pour l'interprétation i. A vous de proposer des implantations de VariableSet et d'Interprétation qui permet ce fonctionnement.

2.5. Interprétations d'une formule (1 pt)

Une instance de la classe/interface VariableSet doit contenir une fonction public List<Interpretation> getInterpretations() qui permet de créer la liste de toutes les interprétations possibles à partir des variables contenues dans l'instance de VariableSet.

3. Formes normales

Cette partie du travail est axée sur les formes normales des formules de la logique propositionnelle.

3.1. Forme Normale simple (2 pt)

La classe/interface Formula doit proposer une méthode Formula toNormalForm() qui retourne une nouvelle instance de Formula représentant la forme normale de l'instance courante.

3.2. Forme Normale Conjonctive (3 pt)

La classe/interface de Formula doit proposer une méthode Formula toCNF() qui retourne une nouvelle instance de Formula représentant la forme normale conjonctive (CNF) de l'instance courante.

3.3. Forme Normale Disjonctive (3 pt)

La classe/interface de Formula doit proposer une méthode Formula toDNF() qui retourne une nouvelle instance de Formula représentant la forme normale disjonctive (DNF) de l'instance courante.

4. Implantation de la méthode des tableaux

La méthode des tableaux (décrite dans le cours relatif à la preuve et au raisonnement) permet de prouver / infirmer automatiquement une formule à partir d'un ensemble d'hypothèses. La forme générale étant la suivante:

$$H_{1},\ \ldots{},\ H_{n}\vdash{}G$$

avec:

• $H_{i}\in{}\mathcal{L}_{p0},\ 1\leq{}i\leq{}n$
• $G\in\mathcal{L}_{p0}$

Vous ajouterez à votre travail précédent sur la représentation de la logique propositionnelle un module permettant de prouver une formule donnée à partir d'un ensemble d'hypothèses lui aussi donné.

5. Représentation d'une déduction

Une déduction s'écrit de la forme $H_{1},\ \ldots{},\ H_{n}\vdash{}G$ où:

• $H_{i}\in{}\mathcal{L}_{p0},\ 1\leq{}i\leq{}n$ est un ensemble hypothèses
• $G\in\mathcal{L}_{p0}$ est une conclusion

Etendre la représentation des formules propositionnelles définie au TP 1 en y ajoutant une classe Deduction qui contient un ensemble d'hypothèses et une conclusion étant toutes des Formule.

6. Lecture d'une déduction en LaTeX

Modifier le module de lecture d'une formule écrite en LaTeX développé lors du TP 1 afin d'y ajouter la possibilité de lire une déduction écrite sous la forme:

$$H_{1},\ \ldots{},\ H_{n}\vdash{}G$$

Par exemple, la déduction $a\vee b, a \vdash a \rightarrow b$ s'écrit en LaTex:

$a \vee b, a \vdash a \rightarrow b$

le symbole $\vdash{}$ etant représenté par \vdash.

3. Implantation de la méthode des Tableaux

Implanter la méthode des tableaux afin de valider une Deduction donnée. Pour cela, ajouter la méthode

boolean isProved()

à la classe Deduction. Cette méthode calculera si la déduction est prouvée grâce à la méthode des tableaux et retournera true si la déduction est prouvée ou false sinon.

4. Test de la méthode

Une fois la méthode implantée, vous testerez son fonctionnement étudiant la démonstration:

$$((p\rightarrow{}r)\wedge{}(q\leftrightarrow{}s)\wedge{}(r\leftrightarrow{}p)\wedge{}p)\vdash{}s$$