Bonsoir,

Je cherche à automatiser la méthode des tableaux (arbre de Beth) en logique propositionnelle classique.

https://fr.wikipedia.org/wiki/M%C3%A9thode_des_tableaux

Je n'arrive pas à définir le sous-algorithme qui prend en paramètre une expression bien formée en chaîne
et qui rend l'arbre binaire de hauteur minimum de sous-chaînes formée à partir des règles.

Pouvez-vous m'aiguiller ?

Merci.

Cordialement,