Trouvez des preuves d'équation dans la logique booléenne
La fonction FindEquationalProof peut construire une preuve d'un théorème à partir d'un ensemble d'axiomes s'ils sont tous exprimés sous forme équationnelle, c'est-à-dire des égalités entre formules construites à partir des opérateurs de la théorie.
Utilisez AxiomaticTheory pour obtenir une collection d'axiomes pour une théorie, comme la logique booléenne. Vous pouvez spécifier les noms des opérateurs et des constantes impliqués. Les variables liées sont représentées à l'aide de symboles formels comme a, b, c.
Construisez la preuve d'une équation.
Affichez la preuve sous la forme d'un graphe montrant le flux de lemmes allant des axiomes (carrés verts) à la conclusion (carré rouge). Les triangles et les cercles représentent différents types de lemmes.
Vous pouvez également afficher tous les détails sur les étapes de l'épreuve.
