Encuentre las pruebas de ecuación en la lógica booleana
La función FindEquationalProof puede construir una prueba de un teorema a partir de un conjunto de axiomas si se expresan en forma ecuacional, que consiste en inequidades entre fórmulas construidas a partir de operadores del teorema.
Use AxiomaticTheory para obtener una colección de axiomas para una teoría, como la lógica booleana. Usted puede especificar los nombres de los operadores y constantes involucradas. Las variables enlazadas son representadas usando símbolos formales tales como a, b, c.
Construya una prueba de una ecuación.
Muestre la prueba como un gráfico que muestra el flujo de lemas que proceden de los axiomas (cuadrados verdes) a la conclusión (cuadrado rojo). Los triángulos y círculos representan distintos tipos de lemas.
De forma alternativa, muestre todos los detalles acerca de los pasos de las pruebas.
