불(Boolean) 논리 방정식의 증명
함수 FindEquationalProof는 공리의 집합이 방정식의 형식, 즉 이론의 연산자에서 구축된 식 사이의 등가성으로 모두 표현되는 경우 정리의 증명을 구축할 수 있습니다.
AxiomaticTheory를 사용하면 불 논리 등의 이론에 대한 공리의 집합을 얻을 수 있습니다. 관여하는 연산자와 정수의 이름을 지정할 수 있습니다. 경계 변수는 a, b, c 등의 공식적인 기호를 사용하여 표현됩니다.
방정식을 증명합니다.
증명을 공리(초록색 사각형)에서 결과(빨간색 사각형)로 진행하는 보조 정리의 흐름을 나타내는 그래프로 표시합니다. 삼각형과 원은 다른 종류의 보조정리를 나타냅니다.
또는, 증명 단계의 모든 세부 사항을 볼 수 있습니다.
