TigerCow.Door


안녕하세요.

지난 포스팅에서는 명제 정리 증명에 있어서 필요한 몇가지 개념에 대해서 알아보았습니다.

이번에는 증명을 이끌어 내는데 사용할 수 있는 추리 규칙(Inference rule)에 대해서 알아보도록 하겠습니다.


1. 전건 긍정(Modus Ponens)


증명이라는 것은 어떤 원하는 목표로 향해가는 결론들, 문장들의 사슬입니다.

그러한 증명을 만들어 내는데 사용되는 가장 잘 알려진 규칙은 아래와 같이 표기하는 전건 긍정(Modus Ponens)입니다.



위의 표기는, 와  형태의 임의의 문장들이 주어졌을 때, 문장 를 추리할 수 있다는 것입니다.



2. 논리곱 소거(AND-elimination)


또 다른 유용한 추리규칙으로는 논리곱 소거(AND-elimination)이 있습니다.

논리곱으로 주어진 문장에서 임의의 논리곱 성분을 추리할 수 있음을 뜻하며 다음과 같이 표기합니다.



와 같은 논리곱 문장의 참(True) 또는 거짓(False)를 알고 있기 때문에, 임의의 논리곱 성분( 또는 ) 또한 알 수 있습니다.



3. 건전한 추리(Sound inference)


 와 의 가능한 진릿값들을 생각해본다면 전건 긍정과 논리곱 소거 모두 전적으로 건전한 추리임을 알수 있기 때문에, 위에서 알아본 두가지 추리규칙을 통해 전체적인 모형을 열거하지 않고도 건전한 추리를 이끌어 낼 수 있습니다.


지난 포스팅에서 모형점검방식으로 다루어 보았던 웜푸스 세계에 대해서 이 추리 규칙들과 동치들을 활용해보도록 하겠습니다.


- [1,1]에 구덩이가 없다.

   R1 : 


- 에이전트가 하나의 칸에 존재함 그 이웃칸에 구덩이가 있으면, 그리고 오직 그럴때에만 미풍을 지각할 수 있다.

   R2 : 

   R3 : 


- 앞의 문장들은 모든 웜푸스 세계에서 참이다. 이제 에이전트가 있는 특정한 세계에서 처음 방문한 두 칸에 대한 미풍 지각을 위한 문장들을 명시한다.

   R4 : 

   R5 : 


출처: http://doorbw.tistory.com/39?category=679148 [Tigercow.Door]


목표는 [1,2]에 구덩이가 없음을, 즉 가 참임을 증명하는 것입니다.


우선 R2에서 상호조건 소거를 적용하여 다음을 얻도록 합니다.

R6 : 


그리고 위에서 알아본 논리곱 소거를 이용해서 다음을 얻습니다.

R7 : 


이어서, R7에 대한 대우 명제를 통해 논리적 동치 명제를 얻습니다.

R8 : 


그리고 R8과 사전에 지식기지에 있던 R4로 전건 긍정을 적용하여 다음을 얻을 수 있습니다.

R9 : 


그리고 드모르간 법칙을 적용하여 다음과 같은 결론을 얻을 수 있습니다.

R10 : 


R10을 통해 [1,2]와 [2,1]에는 구덩이가 없다는 것을 알 수 있습니다.


이러한 증명을 손으로 직접 이끌어 내었지만, 임의의 검색 알고리즘을 이용해서 증명을 구성하는 일련의 단계들을 찾아내는 것도 가능합니다. 증명 문제를 다음과 같이 정의하기만 하면 됩니다.


초기상태(Initial-State) : 초기 지식 기반

동작들(Actions) : 추리 규칙의 상단 절반에 부합하는 모든 문장에 적용되는 모든 추리 규칙에 해당하는 동작들의 집합

결과(Result) : 한 동작의 결과는 문장을 추리 규칙의 하단 절반에 추가하는 것

목표(Goal) : 목표는 증명하고자 하는 문장을 담은 상태


즉, 증명을 찾는 것은 모든 모형들을 열거하는 방법의 한 대안입니다. 실제 문제들에서는 증명을 찾는 것이 더 효율적인 경우가 많은데, 이는 증명과 무관한 명제들은 무시할 수 있기 때문입니다.



4. 단조성(monotonicity)


논리 체계에서 마지막으로 살펴볼 것은 단조성(monotonicity)입니다. 이는 특정 지식기지에 정보, 문장이 추가된다면 이는 함축된 문장들의 집합이 항상 커지기만을 의미할 뿐이지, 추가된 것에 의해 이미 추리된 결론이나 기타 결론에 영향을 주지 않는다는 것입니다.

즉, 지식 기지에서 추리를 통해 얻어낸 결론 A가 존재할 때, 또 다른 단언 명제 B가 추가된다면 이는 추가적인 결론들을 이끌어내는데 도움이 될 수도 있겠지만, 이미 추리된 결론 A는 무효화되지 않습니다.

단조성을 통해 우리는 지식 기지에서 적절한 전제를 찾았다면 언제라도 추리 규칙들을 적용할 수 있음을 알 수 있습니다.

추리 규칙의 결론은 지식 기지에 있는 또 다른 지식과는 무관하게 옳아야 하기 때문입니다.


이렇게 하여 증명을 이끌어 내는 몇가지 추리규칙과 단조성에 대해서 알아보았습니다.

다음 포스팅에서는 분해증명에 대해서 알아보도록 하겠습니다.

블로그 이미지

Tigercow.Door

Web Programming / Back-end / Database / AI / Algorithm / DeepLearning / etc