Ce TP est la suite directe du TP 1. Il s'agit de compléter les fonctionnalités liées à la logique propositionnelles développées en y ajoutant un système de preuves par la méthode des tableaux.

Vous avez toute liberté pour réaliser les demandes de ce projet du moment que vous respectez les contraintes suivantes:

• Le travail sera obligatoirement en solo.
• Le projet doit être réalisé en Java
• La représentation des données et les algorithmes demandés doivent être complètement implantés et, sauf mention contraire, ne doivent pas déléguer leur traitement à une librairie.

Le résultat du TP sera évalué par une rapide présentation des fonctionnalités à l'enseignant et par une étude du code a postériori.

Utilisation d'outils d'aide par l'IA

L'utilisation d'outils d'aide d'IA (ChatGPT, Copilot, Grok, ...) sera intégrée à la notation de la façon suivante:

• Un travail rendu sans aucune aide d'IA sera noté sur une base de 100%
• Un travail réalisé avec l'aide d'IA et déclaré comme tel sera noté sur une base de 60%
• Un travail rendu, réalisé avec l'aide de l'IA sans que cela soit explicitement déclaré sera noté sur une base de 30%

1. 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é.

2. 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.

3. 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$$