2개의 가설: {여왕은 성을 가지고 있다. 앨리스는 성을 가지고 있지 않다.}로부터 결론 "앨리스는 여왕이 아니다."를 도출하겠습니다. 결론의 부정을 가설로 삼아 3개의 논리식으로부터 출발하여 아래와 같이 논리도해를 구성합니다. 이 논리도해는 총 3개의 가지가 있는데, 각각의 가지에 x표 되었으므로 라인 1,2,3의 집합은 만족불가능임이 증명되었습니다.
위의 논리도해는 터뜨리기만 3번 사용하여 작성하였습니다. 이제 아래의 논리도해를 봅시다. 이 논리도해는 터뜨리기 2번, 그리고 추론을 1번 사용하였습니다.
- 추론을 사용하여 얻은 논리식은 5번 라인입니다. 주석을 보면 라인 4와 2를 전제로 사용했음을 알 수 있습니다. 그리고 4번과 2번으로부터 5번을 얻은 것은 흔히 modus ponens라고 알려진 추론규칙을 적용한 결과입니다. 이 추론규칙은 → 소거라고 부르기도 하고 또는 modus ponendo ponens라고 하기도 하는데, 우리는 이 3번째 용어를 번역한 예예(yes yes)규칙이라는 명칭을 사용하기로 합니다.
- 논리도해에서 추론을 사용하는 이론적 근거는 간단합니다: 어떤 논리도해의 어떤 가지를 이루는 논리식을 A1,...,An이라 했을 때 만일 A1,...,An \(\models\) B라면, Mod(A1,...,An) = Mod(A1,...,An,B)라는 것입니다.
- 논리도해에서 추론을 사용하려면 전제 라인의 클릭구역을 오른쪽마우스클릭한 다음, 현재 포커스 된 라인의 클릭구역을 더블클릭합니다. 이렇게 하면 추론에 의하여 얻은 (새로운) 논리식이 포커스 된 라인 바로 아래에 들어가게 됩니다.
논리도해 프로그램 사용법
- 작성한, 혹은 작성중인 논리도해를 보관하려면 [출력]을 클릭합니다. 팝업창에 논리도해를 인코딩한 소스가 나타날 것입니다. 이것을 마우스로 선택(select)하고 시스템 버퍼에 복사(Ctrl-C)한 후 텍스트 파일, 혹은 워드 프로세서 문서에 붙여넣기(Ctrl-V)하면 됩니다.
- 저장된 논리도해를 읽어 들이려면 문서 파일에서 해당 소스를 선택, 복사 후 논리도해 화면에서 [입력]을 클릭하여 나타나는 팝업창에 붙여 넣고, 팝업창의 버튼 [Go]를 클릭하면 됩니다.
- 가지치기로 생성된 라인 둘 중에 어느 하나만 삭제할 수는 없습니다. 무결성(integrity)가 훼손되기 때문입니다. 가지치기로 생성된 두 가지를 모두 삭제하려면 그 가지들의 부모노드(parent node)에 속하는 라인 중 하나에 포커스를 둔 상태에서 [부분나무 삭제]를 클릭합니다. 예를 들어 [앨리스는 여왕이 아니다]의 첫번째 증명에서 라인 8과 9를 동시에 삭제하려면 라인 7에 포커스를 두고 [부분나무 삭제]를 클릭합니다. 라인 6,7,8,9를 삭제하려면 라인 1,2,3,4,5 중 어느 하나에 포커스를 두고 [부분나무 삭제]를 클릭합니다.
- 논리도해에서 라인을 삭제, 추가, 변경했을 때 무결성이 훼손되었는지 알아 보려면 [무결성 검사]를 클릭합니다. 그러면 입증되지 않은 라인들이 붉은 x표로 표시됩니다.
[돌아가기]