Tigercow.Door

안녕하세요.지난 포스팅에서는 명제 정리 증명에 있어서 필요한 몇가지 개념에 대해서 알아보았습니다.이번에는 증명을 이끌어 내는데 사용할 수 있는 추리 규칙(Inference rule)에 대해서 알아보도록 하겠습니다.1. 전건 긍정(Modus Ponens) 증명이라는 것은 어떤 원하는 목표로 향해가는 결론들, 문장들의 사슬입니다.그러한 증명을 만들어 내는데 사용되는 가장 잘 알려진 규칙은 아래와 같이 표기하는 전건 긍정(Modus Ponens)입니다. 위의 표기는, 와 형태의 임의의 문장들이 주어졌을 때, 문장 를 추리할 수 있다는 것입니다. 2. 논리곱 소거(AND-elimination) 또 다른 유용한 추리규칙으로는 논리곱 소거(AND-elimination)이 있습니다.논리곱으로 주어진 문장에서 임의의 ..

안녕하세요. 문범우입니다.이번 포스팅 부터 약 2~3번에 거쳐 명제 정리 증명에 대한 이야기를 해보겠습니다.먼저 오늘은 정리 증명 알고리즘의 세부사항에 앞서, 함축과 관련된 몇가지 추가적인 개념을 알아보도록 하겠습니다.1. 명제 정리 증명 개요 지난 포스팅을 통해 우리는 모든 모형들을 열거하면서 문장이 모든 모형에서 성립하는지 점검하는 모형 점검 방식에 대해 알아보았습니다. 이제는 정리 증명(Theorem proving)을 이용하여 함축 관계를 확인하는 방법에 대해서 알아보겠습니다. 우리가 앞으로 알아볼 접근 방식에서는 주어진 문장의 증명을 구축하여 함축관계를 확인하기 위해서 지식 기지(KB)에 있는 문장들에 여러가지 추리 규칙들을 적용할 것 입니다. 우리가 앞에서 살펴본 모형 점검 방식에 비해, 모형이..