개요
추론 규칙은 프로그래밍 언어에서 syntax가 어떤 규칙을 따라가야하는지 수학적 기호로 표현한 것을 말한다. 추론 규칙은 마치 분수처럼 나타내지는데, 분자부분에는 추론들의 집합이, 분모 부분에는 추론의 결과가 있다. 추론들의 집합을 모두 만족시키는 결과가 분모임의 나타낸다. (모든 Hypothesis가 참이면 C임의 나타낸다.)
- [math]\begin{array}{c} {H_1 \qquad H_2 \qquad ... \qquad H_n } \\\hline {Conclusion} \end{array}[/math]
는 다음과 같은 의미이다.
- [math]H_1 \wedge H_2 \wedge ... \wedge H_n \Rightarrow Conclusion [/math]
예시
- [math]\begin{array}{c} {n \in \mathbb{Z}} \\\hline {n \in A} \end{array}[/math]
- [math]\begin{array}{c} {e_1 \in A \qquad e_2 \in A} \\\hline {e_1 + e_2 \in A} \end{array}[/math]
- [math]\begin{array}{c} {e_1 \in A \qquad e_2 \in A} \\\hline {e_1 - e_2 \in A} \end{array}[/math]
과 같은 추론 규칙이 주어졌다고 할때, [math]4 + (2 - 1) \in A [/math]임을 증명해 보자.
- [math]\begin{array}{c} {\begin{array}{c} {4 \in \mathbb{Z}} \\\hline 4 \in A \end{array} \qquad \begin{array}{c} {\begin{array}{c} {2 \in \mathbb{Z}} \\\hline 2 \in A \end{array} \begin{array}{c} {1 \in \mathbb{Z}} \\\hline 1 \in A \end{array}} \\\hline 2 - 1 \in A \end{array}} \\\hline 4 + (2 - 1) \in A \end{array}[/math]
위에서 정의된 추론 규칙에 의해서 주어진 식은 같이 A에 속함을 증명할 수 있다.