Si un projet Java existant est utilisé, lui ajouter le package fr.utln.logic.firstorder qui permettra d'implanter les classes et interfaces nécessaires à la représentation de la logique du premier-ordre.

Il est également possible de commencer à partir d'un projet pré-configuré avec Maven et disponible ici qui contient déjà le package demandé.

Dans le package fr.utln.logic.firstorder, ajouter une interface Formula, qui permettra de représenter une formule. Cette interface est pour le moment vide et sera complétée au fur et à mesure de l'avancée de ce travail.

Dans le projet Java, ajouter un package fr.utln.logic.firstorder.term qui permettra de rassembler les classes et interfaces liées aux termes de la logique du premier-ordre. Ce package devra contenir une interface Term représentant un terme. L'interface Term déclarera la méthode String getName() qui servira à récupérer le nom du terme.

Dans le package fr.utln.logic.firstorder.term ajouter:

• une classe Var qui implante Term et qui contient
  • un constructeur public Var(String name) prenant en paramètre le nom de la variable représentée;
  • la surcharge de la méthode public String toString() qui retourne le nom de la variable;

• une classe Constant qui implante Term et qui contient:
  • un constructeur public Constant(String name) prenant en paramètre le nom de la constante représentée;
  • la surcharge de la méthode public String toString() qui retourne le nom de la constante;

Penser à implanter les méthodes issues de l'interface Term.

Dans le package fr.utln.logic.firstorder.term ajouter une classe Function qui implante l'interface Term et qui contient:

• un champ private final List<Term> arguments qui stocke les arguments de la fonction;
• un constructeur public Function(String name, Term term) qui crée une fonction nommée name dont l'argument unique est term;
• un constructeur public Function(String name, List<Term> terms) qui crée une fonction nommée name dont les arguments sont terms;
• un constructeur public Function(String name, Term... terms) qui crée une fonction nommée name dont les arguments sont terms;
• une méthode public List<Term> getArguments() qui retourne les arguments (termes) de la fonction;
• la surcharge de la méthode public String toString() qui retournera l'affichage textuel de la fonction sous la forme standard f(a1, ..., an).

Penser à implanter les méthodes de l'interface Term.

Dans le package fr.utln.logic.firstorder ajouter une classe Predicate qui implante l'interface Formula et qui contient:

• un champ private final List<Term> arguments qui stocke les arguments du prédicat
• un constructeur public Predicate(String name, Term term) qui crée un prédicat nommé name dont l'argument unique est term
• un constructeur public Predicate(String name, List<Term> terms) qui crée un prédicat nommé name dont les arguments sont terms
• un constructeur public Predicate(String name, Term... terms) qui crée un prédicat nommé name dont les arguments sont terms
• une méthode public String getName() qui retourne le nom du prédicat
• une méthode public List<Term> getArguments() qui retourne les arguments (termes) de la prédicat
• la surcharge de la méthode public String toString() qui retournera l'affichage textuel du prédicat sous la forme standard p(a1, ..., an) ou juste p si le prédicat n'a pas d'argument

Rappel: Contrairement à une fonction, un prédicat peut ne pas avoir d'argument (on l'appelle alors prédicat 0-aire ou proposition primitive)

Ajouter un package fr.utln.logic.firstorder.example au projet et y ajouter une classe Example01 dont le code est le suivant:

package fr.utln.logic.firstorder.example;

import fr.utln.logic.firstorder.Predicate;
import fr.utln.logic.firstorder.term.Constant;
import fr.utln.logic.firstorder.term.Function;
import fr.utln.logic.firstorder.term.Term;
import fr.utln.logic.firstorder.term.Var;

/**
 * A first example of first-order logic API.
 * @author Julien Seinturier - Universit&eacute; de Toulon / LIS umr CNRS 7020 - <a href="http://web.seinturier.fr">http://web.seinturier.fr</a>
 */
public class Example01 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        Var a = new Var("a");
        Var b = new Var("b");

        Constant c = new Constant("c");

        Term f = new Function("f", a, b);
        Term g = new Function("g", a, c);
        Term h = new Function("h", b, c);

        Predicate p = new Predicate("P", f, g);
        Predicate q = new Predicate("Q");

        System.out.println("Variables: ");
        System.out.println("  a: "+a);
        System.out.println("  b: "+b);

        System.out.println("Constants: ");
        System.out.println("  c: "+c);

        System.out.println("Functions: ");
        System.out.println("  f: "+f);
        System.out.println("  g: "+g);
        System.out.println("  h: "+h);

        System.out.println("Predicates: ");
        System.out.println("  p: "+p);
        System.out.println("  q: "+q);
    }
}

Le résultat de l'exécution de la classe Example01 attendu est le suivant:

Variables: 
  a: a
  b: b
Constants: 
  c: c
Functions: 
  f: f(a, b)
  g: g(a, c)
  h: h(b, c)
Predicates: 
  p: P(f(a, b), g(a, c))
  q: Q

S'il ne s'agit pas du résultat affiché, il faut reprendre les classes des exercices 2 à 6 et les corriger.

Ajouter au projet un package fr.utln.logic.firstorder.connector et y ajouter une interface Connector qui permet de représenter un connecteur logique et qui déclare la fonction public Formula[] getOperands() qui retourne les opérandes liées par ce connecteur.

Dans le package fr.utln.logic.firstorder.connector, ajouter:

• une interface UnaryConnector qui:
  • étend l'interface Connector
  • déclare la méthode Formula getOperand() retournant l'opérande liée à ce connecteur

• une interface BinaryConnector qui:
  • étend l'interface Connector 
  • déclare la méthode Formula getOperandLeft() qui retourne l'opérande gauche du connecteur
  • déclare la méthode Formula getOperandRight() qui retourne l'opérande droite du connecteur
  • déclare un champ int LEFT = 0 (pour repérer l'opérande gauche)
  • déclare un champ int RIGHT = 1 (pour repérer l'opérande droit)
  •  

Dans le package fr.utln.logic.firstorder.connector, ajouter:

• une classe abstraite AbstractUnaryConnector qui:
  • implante l'interface UnaryConnector
  • possède un champ private final Formula formula permettant de gérer l'opérande
  • possède un constructeur public AbstractUnaryConnector(Formula formula) pour initialiser l'opérande

• une classe abstraite AbstractBinaryConnector qui:
  • implante l'interface BinaryConnector 
  • possède un champ private final Formula[] formulas permettant de gérer les opérandes gauche et droite
  • possède un constructeur public AbstractBinaryConnector(Formula left, Formula right) pour initialiser les opérandes

Dans le package fr.utln.logic.firstorder.connector, ajouter:

• une classe Not qui:
  • étend la classe AbstractUnaryConnector
  • implante l'interface Formula
  • possède un constructeur public Not(Formula formula) permettant de construire la négation \( \neg \)formula 
  • possède une méthode public String toString() renvoyant la représentation textuelle de la formule (indice: \( \neg \) s'écrit en Unicode '\u00AC')

• une classe And qui:
  • étend la classe AbstractBinaryConnector 
  • implante l'interface Formula
  • possède un constructeur public And(Formula left, Formula right) permettant de construire la conjonction left \( \wedge \) right
  • possède une méthode public String toString() renvoyant la représentation textuelle de la formule (indice: \( \wedge \) s'écrit en Unicode '\u2227')

• une classe Or qui:
  • étend la classe AbstractBinaryConnector 
  • implante l'interface Formula
  • possède un constructeur public Or(Formula left, Formula right) permettant de construire la disjonction left \( \vee \) right
  • possède une méthode public String toString() renvoyant la représentation textuelle de la formule (indice: \( \vee \) s'écrit en Unicode '\u2228')

• une classe Imp qui:
  • étend la classe AbstractBinaryConnector 
  • implante l'interface Formula
  • possède un constructeur public Imp(Formula left, Formula right) permettant de construire l'implication left \( \to \) right
  • possède une méthode public String toString() renvoyant la représentation textuelle de la formule (indice: \( \to \) s'écrit en Unicode '\u2192')

• une classe Equiv qui:
  • étend la classe AbstractBinaryConnector 
  • implante l'interface Formula
  • possède un constructeur public Equiv(Formula left, Formula right) permettant de construire l'équivalence left \( \leftrightarrow \) right
  • possède une méthode public String toString() renvoyant la représentation textuelle de la formule (indice: \( \leftrightarrow \) s'écrit en Unicode '\u2194')

Attention: Penser à bien appeler le constructeur des classes abstraites dans chacun des cas.

Dans le package fr.utln.logic.firstorder.example, ajouter une classe Example02 dont le code est le suivant:

package fr.utln.logic.firstorder.example;

import fr.utln.logic.firstorder.Formula;
import fr.utln.logic.firstorder.Predicate;
import fr.utln.logic.firstorder.connector.*;
import fr.utln.logic.firstorder.term.Function;
import fr.utln.logic.firstorder.term.Term;
import fr.utln.logic.firstorder.term.Var;

/**
 * A second example of first-order logic API.
 * @author Julien Seinturier - Universit&eacute; de Toulon / LIS umr CNRS 7020 - <a href="http://web.seinturier.fr">http://web.seinturier.fr</a>
 */
public class Example02 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        Var a = new Var("a");
        Var b = new Var("b");
        Var x = new Var("x");
        Var y = new Var("y");

        Term f = new Function("f", x, y);

        Predicate p = new Predicate("P", a);
        Predicate q = new Predicate("Q", b);
        Predicate r = new Predicate("R", f);

        Not not = new Not(p);
        Or or = new Or(r, p);
        And and = new And(p, r);
        Imp imp = new Imp(r, q);
        Equiv equ = new Equiv(q, p);

        Formula formula = new Not(new And(new Or(new Or(p, q), r), new Imp(r, q)));

        System.out.println("NOT: "+not);
        System.out.println("  Operand: "+not.getOperand());
        System.out.println();
        System.out.println("AND: "+and);
        System.out.println("  L operand: "+and.getOperandLeft());
        System.out.println("  R operand: "+and.getOperandRight());
        System.out.println();
        System.out.println("OR : "+or);
        System.out.println("  L operand: "+or.getOperandLeft());
        System.out.println("  R operand: "+or.getOperandRight());
        System.out.println();
        System.out.println("IMP: "+imp);
        System.out.println("  L operand: "+imp.getOperandLeft());
        System.out.println("  R operand: "+imp.getOperandRight());
        System.out.println();
        System.out.println("EQU: "+equ);
        System.out.println("  L operand: "+equ.getOperandLeft());
        System.out.println("  R operand: "+equ.getOperandRight());
        System.out.println();
        System.out.println("Formula: "+formula);
    }
}

L'affichage attendu est alors:

NOT: ¬P(a)
  Operand: P(a)

AND: P(a) ∧ R(f(x, y))
  L operand: P(a)
  R operand: R(f(x, y))

OR : R(f(x, y)) ∨ P(a)
  L operand: R(f(x, y))
  R operand: P(a)

IMP: R(f(x, y)) → Q(b)
  L operand: R(f(x, y))
  R operand: Q(b)

EQU: Q(b) ↔ P(a)
  L operand: Q(b)
  R operand: P(a)

Formula: ¬P(a) ∨ Q(b) ∨ R(f(x, y)) ∧ R(f(x, y)) → Q(b)

Si l'affichage n'est pas correct, reprendre les exercices 8, 9, 10 et 11 afin de faire les correction qui s'imposent.

En s'intéressant au code de la dernière formule affichée:

Formula formula = new Not(new And(new Or(new Or(p, q), r), new Imp(r, q)));

et en observant l'affichage produit:

Formula: ¬P(a) ∨ Q(b) ∨ R(f(x, y)) ∧ R(f(x, y)) → Q(b)

que remarque-t-on ? (indice: la formule codée est \(\neg{}((P(a)\vee{}Q(b)\vee{}R(f(x,y)))\wedge{}(R(f(x,y))\to{}Q(b)))\)

Editer l'interface Formula et y ajouter une méthode String toStringStrict() afin d'indiquer qu'une formule peut être affichée sous forme stricte.

Cette modification entraine maintenant la nécessité d'implanter cette nouvelle méthode dans toutes les classes héritant de Formula, à savoir:

• Predicate
• Neg
• And
• Or
• Imp
• Equiv

Réaliser les implantations nécessaires afin de s'assurer de l'affichage strict d'une formule lors d'un appel à toStringStrict().

Rappel: Les parenthèses à ajouter ne concerne que les connecteurs binaires. L'appel à toStringStrict() pour Predicate ou Neg doit donc pas ajouter de parenthèses.

Editer la classe Example02 et ajouter à la fin de la méthode main (juste après les System.out.println() déjà en place) la ligne:

System.out.println("Strict : "+formula.toStringStrict());

Exécuter la classe Example02 pour vérifier si l'affichage des formules strictes est opérationnel. Le résultat attendu est:

NOT: ¬P(a)
  Operand: P(a)

AND: P(a) ∧ R(f(x, y))
  L operand: P(a)
  R operand: R(f(x, y))

OR : R(f(x, y)) ∨ P(a)
  L operand: R(f(x, y))
  R operand: P(a)

IMP: R(f(x, y)) → Q(b)
  L operand: R(f(x, y))
  R operand: Q(b)

EQU: Q(b) ↔ P(a)
  L operand: Q(b)
  R operand: P(a)

Formula: ¬P(a) ∨ Q(b) ∨ R(f(x, y)) ∧ R(f(x, y)) → Q(b)
Strict : ¬(((P(a) ∨ Q(b)) ∨ R(f(x, y))) ∧ (R(f(x, y)) → Q(b)))

Ajouter au projet le package fr.utln.logic.firstorder.quantifier et y ajouter une interface Quantifier qui représente un quantificateur de la logique du premier ordre. Cette interface contient : 

• une méthode Var getVariable() qui retourne la variable associée au quantificateur
• une méthode Formula getFormula() qui retourne la formule quantifiée

Dans le  le package fr.utln.logic.firstorder.quantifier, ajouter une classe abstraite AbstractQuantifier qui permet de gérer la variable et la formule associées à un quantificateur quelconque. Cette classe abstraite: 

• étend l'interface Quantifier
• possède un champ private final Var variable pour stocker la variable associée
• possède un champ private final Formula formula pour stocker la formule quantifiée
• possède un constructeur public AbstractQuantifier(Variable v, Formula f) qui initialise les champs variable et formula
• implante la méthode getVariable() de Quantifier
• implante la méthode getFormula() de Quantifier

Dans le  le package fr.utln.logic.firstorder.quantifier, ajouter:

• Une classe Forall qui représente le quantificateur universel \( \forall{} \) et qui:
  • étend la classe abstraite AbstractQuantifier
  • implante l'interface Formula
  • possède un constructeur public Forall(Var variable, Formula formula) (penser à appeler le constructeur parent)
  • redéfini la méthode public String toString() en retournant "∀<variable><formula>" (le caractère unicode de \( \forall \) étant '\u2200') 
  • implante la méthode public String toStringStrict() en retournant "∀<variable>(<formula>)"

• Une classe Exists qui représente le quantificateur existentiel \( \exists{} \) et qui:
  • étend la classe abstraite AbstractQuantifier
  • implante l'interface Formula
  • possède un constructeur public Exists(Var variable, Formula formula) (penser à appeler le constructeur parent)
  • redéfini la méthode public String toString() en retournant "∃<variable><formula>" (le caractère unicode de \( \exists \) étant '\u2203') 
  • implante la méthode public String toStringStrict() en retournant "∀<variable>(<formula>)"
  •  

Dans le package fr.utln.logic.firstorder.example, ajouter la classe Example03 dont le code est le suivant: 

import fr.utln.logic.firstorder.quantifier.ForAll;
import fr.utln.logic.firstorder.term.Function;
import fr.utln.logic.firstorder.term.Term;
import fr.utln.logic.firstorder.term.Var;

/**
 * A third example of first-order logic API. This example focuses on quantifiers.
 * @author Julien Seinturier - Universit&eacute; de Toulon / LIS umr CNRS 7020 - <a href="http://web.seinturier.fr">http://web.seinturier.fr</a>
 */
public class Example03 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        Var x = new Var("a");
        Var y = new Var("b");
        Var z = new Var("x");

        Term f = new Function("f", x, y);

        Predicate p = new Predicate("P", x, y);
        Predicate q = new Predicate("Q", z);
        Predicate r = new Predicate("R", f);


        Formula formula1 = new ForAll(x, new And(new Or(new Or(p, q), r), new Imp(r, q)));

        Formula formula2 = new Exists(y, new Or(new And(new And(p, q), r), new Imp(r, q)));

        System.out.println("Formula 1: "+formula1);
        System.out.println("  Strict : "+formula1.toStringStrict());
        System.out.println();
        System.out.println("Formula 2: "+formula2);
        System.out.println("  Strict : "+formula2.toStringStrict());

    }

}

Exécuter la classe, l'affichage attendu sur la console est le suivant:

Formula 1: ∀a P(a, b) ∨ Q(x) ∨ R(f(a, b)) ∧ R(f(a, b)) → Q(x)
  Strict : ∀a (((P(a, b) ∨ Q(x)) ∨ R(f(a, b))) ∧ (R(f(a, b)) → Q(x)))

Formula 2: ∃b P(a, b) ∧ Q(x) ∧ R(f(a, b)) ∨ R(f(a, b)) → Q(x)
  Strict : ∃b (((P(a, b) ∧ Q(x)) ∧ R(f(a, b))) ∨ (R(f(a, b)) → Q(x)))

Si ce n'est pas le cas, les exercice 15, 16 et 17 doivent être repris afin de corriger les erreurs.

Créer un package fr.utln.logic.firstorder.io et y ajouter l'interface FormulaReader qui décrit un objet capable d'instancier une formule du premier-ordre à partir de son expression en texte. Cette interface déclare la méthode:

/**
  * Read the given textual representation and instantiate the corresponding {@link Formula formula}.
  * @param input the textual representation of the formula
  * @return the formula that corresponds to the given input
  */
Formula read(String input);

Dans le  package fr.utln.logic.firstorder.io, ajouter la classe FormulaReaderException qui représente une erreur dans la lecture d'une formule du premier-ordre depuis un texte. Cette classe a pour code:

package fr.utln.logic.firstorder.io;

import java.io.Serial;

/**
 * An exception raised when a textual representation of a formula cannot be read.
 * The exception provides the input and the position within the input where the error has been detected.
 */
public class FormulaReaderException extends RuntimeException {

    @Serial
    private static final long serialVersionUID = 1L;

    /**
     * The input that has been read.
     */
    private final String input;

    /**
     * The position (index of the character) within the input where the error has been detected.
     */
    private final int position;

    /**
     * Create a new parse exception.
     * @param message the description of the error
     * @param input the input that has been read
     * @param position the position (index of the character) within the input where the error has been detected
     */
    public FormulaReaderException(String message, String input, int position) {
        super(message);
        this.input = input;
        this.position = position;
    }

    /**
     * Get the input that has been read.
     * @return the input that has been read
     */
    public String getInput() {
        return this.input;
    }

    /**
     * Get the position (index of the character) within the input where the error has been detected.
     * @return the position where the error has been detected
     */
    public int getPosition() {
        return this.position;
    }

    /**
     * Get a message that describes the error and that shows its location within the input using a caret (<code>^</code>).
     * @return a message that describes and locates the error
     */
    @Override
    public String getMessage() {
        if (this.input == null) {
            return super.getMessage();
        }

        return super.getMessage() + " at position " + this.position + System.lineSeparator()
                + "  " + this.input + System.lineSeparator()
                + "  " + " ".repeat(Math.max(0, Math.min(this.position, this.input.length()))) + "^";
    }
}

Dans le  package fr.utln.logic.firstorder.io, modifier l'interface FormulaReader afin que la méthode read puisse lever l'exception FormulaReaderException. 

Dans le package fr.utln.logic.firstorder.io, ajouter la classe FormulaTokenType qui permettra de gérer les différents types de token utiles à la représentation de formules du premier ordre. Le code de la classe est le suivant:

package fr.utln.logic.firstorder.io;

/**
 * The types of the tokens that can be produced by a formula lexer.
 */
public enum FormulaTokenType {

    /** The negation (¬). */
    NOT,

    /** The conjunction (∧). */
    AND,

    /** The disjunction (∨). */
    OR,

    /** The implication (→). */
    IMP,

    /** The equivalence (↔). */
    EQUIV,

    /** The universal quantifier (∀). */
    FORALL,

    /** The existential quantifier (∃). */
    EXISTS,

    /** An opening parenthesis: <code>(</code>, <code>[</code> or <code>{</code>. */
    LP,

    /** A closing parenthesis: <code>)</code>, <code>]</code> or <code>}</code>. */
    RP,

    /** The argument separator <code>,</code>. */
    CO,

    /** The separator between quantified variables and their formula: <code>.</code> or <code>:</code>. */
    DOT,

    /** An identifier (name of a predicate, a function, a variable or a constant). */
    ID,

    /** The end of the input. */
    EOF
}

Dans le package fr.utln.logic.firstorder.io, ajouter la classe FormulaToken qui permettra de gérer les différents tokens utilisés pour lire une formule du premier ordre. Le code de la classe est le suivant:

package fr.utln.logic.firstorder.io;

/**
 * A formula token produced by a lexer.
 * @param type the type of the token
 * @param text the text of the token (the name for an {@link FormulaTokenType#ID identifier}, the character for a parenthesis)
 * @param position the position (index of the first character) of the token within the input
 * @param end the position that follows the last character of the token within the input
 * @author Julien Seinturier - Universit&eacute; de Toulon / LIS umr CNRS 7020 - <a href="http://web.seinturier.fr">http://web.seinturier.fr</a>
 */
public record FormulaToken(FormulaTokenType type, String text, int position, int end) {

    /**
     * Create a new token whose end is not known yet (the end is set to the position).
     * @param type the type of the token
     * @param text the text of the token
     * @param position the position (index of the first character) of the token within the input
     */
    public FormulaToken(FormulaTokenType type, String text, int position) {
        this(type, text, position, position);
    }

    /**
     * Check if this token is immediately followed by the given token (without any character in between).
     * @param next the token to check
     * @return <code>true</code> if the given token starts exactly where this token ends and <code>false</code> otherwise
     */
    public boolean isAdjacentTo(FormulaToken next) {
        return this.end == next.position;
    }

    @Override
    public String toString() {
        return this.type + (this.text.isEmpty() ? "" : "[" + this.text + "]") + "@" + this.position;
    }
}

Dans le package fr.utln.logic.firstorder.io, ajouter la classe FormulaParser qui réalise l'analyse syntaxique d'une formule du premier ordre exprimée sous-forme tokens et qui produit la représentation Java de cette formule. Le but de ce travail n'étant pas la construction d'un analyseur syntaxique, le code de la classe peut être récupéré ici.

Ajouter le package fr.utln.logic.firstorder.io.unicode au projet et ajouter dans celui-ci la classe UnicodeValues qui permettra de gérer les caractères Unicode intéressants pour la représentation de formules du premier ordre. Le code de la classe est le suivant:

package fr.utln.logic.firstorder.io.unicode;

public class UnicodeValues {

    public static final char NOT_CH = '\u00AC';

    public static final char AND_CH = '\u2227';

    public static final char OR_CH = '\u2228';

    public static final char IMP_CH = '\u2192';

    public static final char EQUIV_CH = '\u2194';

    public static final char FORALL_CH = '\u2200';

    public static final char EXISTS_CH = '\u2203';
}

Dans le package fr.utln.logic.firstorder.io.unicode, ajouter la classe UnicodeLexer qui permettra de découper un texte Unicode en différents tokens utilisés pour construire une formule du premier ordre. Le but de ce travail n'étant pas la construction d'un analyseur lexical, le code de la classe peut être récupéré ici.

Dans le package fr.utln.logic.firstorder.io.unicode, ajouter la classe UnicodeReader qui implante FormulaReader et permet d'instancier une formule du premier-ordre à partir de son expression en texte Unicode. Le code de la classe est le suivant:

package fr.utln.logic.firstorder.io.unicode;

import fr.utln.logic.firstorder.Formula;
import fr.utln.logic.firstorder.Predicate;
import fr.utln.logic.firstorder.io.*;
import fr.utln.logic.firstorder.term.Constant;
import fr.utln.logic.firstorder.term.Function;
import fr.utln.logic.firstorder.term.Var;

import java.util.*;

/**
 * A reader that instantiates a first-order logic {@link Formula formula} from its unicode representation,
 */
public class UnicodeReader implements FormulaReader {

    /**
     * The names of the identifiers that have to be read as constants.
     */
    private final Set<String> constants;

    /**
     * Create a new unicode reader. Without declared constants, the free identifiers used as terms are read as variables
     * (except the numbers that are always read as constants).
     */
    public UnicodeReader() {
        this.constants = new HashSet<>();
    }

    /**
     * Create a new unicode reader that reads the given free identifiers as {@link Constant constants}.
     * @param constants the names of the constants
     */
    public UnicodeReader(String... constants) {
        this();
        declareConstants(constants);
    }

    @Override
    public Formula read(String content) throws FormulaReaderException {

        if (content == null)
            throw new IllegalArgumentException("Input cannot be null");

        List<FormulaToken> tokens = new UnicodeLexer(content).tokenize();

        return new FormulaParser(content, tokens, constants).parse();
    }

    /**
     * Declare the given names as {@link Constant constants}. When they are not bound by a quantifier,
     * the identifiers with these names are read as constants instead of free variables.
     * @param names the names of the constants
     * @return this reader
     * @throws IllegalArgumentException if a name is <code>null</code> or empty
     */
    public UnicodeReader declareConstants(String... names) {
        if (names != null) {
            for (String name : names) {
                if ((name == null) || name.isEmpty())
                    throw new IllegalArgumentException("Constant cannot have empty name.");

                this.constants.add(name);
            }
        }
        return this;
    }

    /**
     * Get the names of the declared {@link Constant constants}.
     * @return the names of the declared constants (unmodifiable)
     */
    public Set<String> getConstants() {
        return Collections.unmodifiableSet(this.constants);
    }

}

Dans le package fr.utln.logic.firstorder.example, ajouter la classe Example04 qui permet de tester la lecture de formule du premier-ordre depuis une expression textuelle Unicode. Le code de la classe est le suivant:

package fr.utln.logic.firstorder.example;

import fr.utln.logic.firstorder.Formula;
import fr.utln.logic.firstorder.Predicate;
import fr.utln.logic.firstorder.connector.And;
import fr.utln.logic.firstorder.connector.Imp;
import fr.utln.logic.firstorder.io.FormulaReader;
import fr.utln.logic.firstorder.io.unicode.UnicodeReader;
import fr.utln.logic.firstorder.quantifier.Exists;
import fr.utln.logic.firstorder.quantifier.ForAll;
import fr.utln.logic.firstorder.term.Function;
import fr.utln.logic.firstorder.term.Var;

/**
 * A third example of first-order logic API. This example focuses on formula I/O.
 */
public class Example04 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        FormulaReader reader = null;

        // Unicode
        String unicode = "\u2200e (P(e) \u2192 \u2203 d ( P(d) \u2227 \u2200 x ( I(m(x, y), d) \u2192 I(m(f(x), f(y)), e))))";

        // Equivalent writing
        //String unicode = "∀e (P(e) → ∃ d ( P(d) ∧ ∀ x ( I(m(x, y), d) → I(m(f(x), f(y)), e))))";

        reader = new UnicodeReader();

        Formula fu = reader.read(unicode);

        System.out.println("Unicode");
        System.out.println("  Text   : \""+unicode+"\"");
        System.out.println("  formula: " + fu);
        System.out.println("  strict : " + fu.toStringStrict());
        System.out.println();

        // Loop
        Formula fr = reader.read(fu.toStringStrict());

        System.out.println("Loop");
        System.out.println("  Text   : \""+fu.toStringStrict()+"\"");
        System.out.println("  formula: " + fr);
        System.out.println("  strict : " + fr.toStringStrict());

    }
}

Ajouter au projet le package fr.utln.logic.firstorder.io.latex, et y ajouter les fichiers suivants:

• LatexLexer.java qui détecte les tokens dans un texte au format LaTeX
• LatexReader.java qui lit une formule du premier-ordre depuis un texte au format LaTeX

Dans le package fr.utln.logic.firstorder.example, modifier la classe Example04 avec le code suivant:

package fr.utln.logic.firstorder.example;

import fr.utln.logic.firstorder.Formula;
import fr.utln.logic.firstorder.io.FormulaReader;
import fr.utln.logic.firstorder.io.latex.LatexReader;
import fr.utln.logic.firstorder.io.unicode.UnicodeReader;

/**
 * A third example of first-order logic API. This example focuses on formula I/O.
 * @author Julien Seinturier - Universit&eacute; de Toulon / LIS umr CNRS 7020 - <a href="http://web.seinturier.fr">http://web.seinturier.fr</a>
 */
public class Example04 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        FormulaReader reader = null;

        // LaTeX
        String latex = "\\forall{}e (P(e) \\to \\exists d ( P(d) \\wedge \\forall x ( I(m(x, y), d) \\implies I(m(f(x), f(y)), e))))";

        reader = new LatexReader();

        Formula fl = reader.read(latex);

        System.out.println("LaTeX");
        System.out.println("  Text   : \""+latex+"\"");
        System.out.println("  formula: " + fl);
        System.out.println("  strict : " + fl.toStringStrict());
        System.out.println();

        // Unicode
        String unicode = "\u2200e (P(e) \u2192 \u2203 d ( P(d) \u2227 \u2200 x ( I(m(x, y), d) \u2192 I(m(f(x), f(y)), e))))";

        // Equivalent writing
        //String unicode = "∀e (P(e) → ∃ d ( P(d) ∧ ∀ x ( I(m(x, y), d) → I(m(f(x), f(y)), e))))";

        reader = new UnicodeReader();

        Formula fu = reader.read(unicode);

        System.out.println("Unicode");
        System.out.println("  Text   : \""+unicode+"\"");
        System.out.println("  formula: " + fu);
        System.out.println("  strict : " + fu.toStringStrict());
        System.out.println();

        // Loop
        Formula fr = reader.read(fl.toStringStrict());

        System.out.println("Loop");
        System.out.println("  Text   : \""+fl.toStringStrict()+"\"");
        System.out.println("  formula: " + fr);
        System.out.println("  strict : " + fr.toStringStrict());

    }
}

Exécuter Example04 et s'assurer que les formules LaTeX sont bien lues.

Reprendre les implantations de la méthode toString() là ou cela est nécessaire afin d'avoir des affichages de formule valides tout en évitant une surcharge de parenthèses.

Afin de proposer un affichage compact, certaines règles peuvent être mises en place:

• Une formule sous la portée d'un quantificateur doit être entre parenthèse sauf si celle-ci débute également par un quantificateur
• Un connecteur suivi d'un connecteur de moindre priorité n'a pas besoin d'être entre parenthèse sauf si plusieurs occurrences de celui-ci se suivent
• Une formule a laquelle est appliquée une négation est entourée de parenthèses sauf si celle-ci débute par un quantificateur ou une négation
• Si une formule est une suite d'implications, celles-ci doivent être parenthésées de droite à gauche

Voici quelques exemples:

Pour tester les implantations, ajouter dans le package fr.utln.logic.firstorder.example la classe Example05 dont le code est:

package fr.utln.logic.firstorder.example;

import fr.utln.logic.firstorder.Formula;
import fr.utln.logic.firstorder.io.FormulaReader;
import fr.utln.logic.firstorder.io.latex.LatexReader;
import fr.utln.logic.firstorder.io.unicode.UnicodeReader;

/**
 * A fifth example of first-order logic API. This example focuses on formula display.
 */
public class Example05 {

    /**
     * The main method
     * @param args the main method arguments
     */
    public static void main(String[] args){

        FormulaReader reader = new UnicodeReader();

        String[] strs = new String[]{"(((a ∧ b) ∧ c) ∨ d)",
                                     "(((a ∨ b) ∨ c) ∧ d)",
                                     "∀a (∃b (P(a) ∨ Q(b)))",
                                     "∀a (∃b (P(a)))",
                                     "∀a (∃b (¬(P(a) → P(b))) ↔ ((a ∧ b) ∧ c))"};
        
        Formula f = null;

        for(String str : strs){

            f = reader.read(str);

            System.out.println("Input      : "+str);
            System.out.println("toString() : "+f);
            System.out.println();
        }

    }
}

Et vérifier si les affichages produits correspondent bien au tableau.

Ajouter à l'interface Formula une methode equals(Formula f) qui renvoie true si la formule courante est syntaxiquement équivalente à f et false sinon. Implanter cette méthode partout là où cela est nécessaire.