Encontre provas equacionais na lógica booleana
A função FindEquationalProof A função pode construir uma prova de um teorema de um conjunto de axiomas se todos eles forem expressos em forma equacional, isto é, igualdades entre fórmulas construídas a partir dos operadores da teoria.
Use AxiomaticTheory para obter uma coleção de axiomas para uma teoria, como a lógica booleana. Você pode especificar os nomes dos operadores e constantes envolvidos. Variáveis vinculadas são representadas usando símbolos formais como a, b, c.
Construa uma prova de uma equação.
Mostre a prova como um gráfico mostrando o fluxo de lemas que vão dos axiomas (quadrados verdes) até a conclusão (quadrado vermelho). Triângulos e círculos representam diferentes tipos de lemas.
Como alternativa, mostre todos os detalhes sobre as etapas da prova.
