안녕하세요. 문범우입니다.
이번 포스팅 부터 약 2~3번에 거쳐 명제 정리 증명에 대한 이야기를 해보겠습니다.
먼저 오늘은 정리 증명 알고리즘의 세부사항에 앞서, 함축과 관련된 몇가지 추가적인 개념을 알아보도록 하겠습니다.
1. 명제 정리 증명 개요
지난 포스팅을 통해 우리는 모든 모형들을 열거하면서 문장이 모든 모형에서 성립하는지 점검하는 모형 점검 방식에 대해 알아보았습니다. 이제는 정리 증명(Theorem proving)을 이용하여 함축 관계를 확인하는 방법에 대해서 알아보겠습니다. 우리가 앞으로 알아볼 접근 방식에서는 주어진 문장의 증명을 구축하여 함축관계를 확인하기 위해서 지식 기지(KB)에 있는 문장들에 여러가지 추리 규칙들을 적용할 것 입니다. 우리가 앞에서 살펴본 모형 점검 방식에 비해, 모형이 많을 수록 또는 정리 증명의 내용이 짧을 수록 보다 효율적인 증명 알고리즘이 될 것입니다.
그리고 먼저, 인사말에서 언급하였듯이 정리 증명 알고리즘의 세부사항에 앞서, 함축과 관련된 몇가지 추가적인 개념을 소개하겠습니다.
2. 논리적 동치(Logical equivalence)
논리적 동치(Logical equivalence)란, 두 문장 a와 b가 동일한 모형들에서 참일 때, 그 두 문장은 동치관계라고 하는 것 입니다. 즉, 논리적 동치라는 개념은 수학에서 항등식과 아주 비슷한 역할을 하는 것 입니다. 이러한 논리적 동치관계는 a
그리고 아래와 같이 정의할 수도 있습니다.
- 임의의 두 문장 a와 b는 만일 하나가 다른 하나를 함축하면, 그리고 오직 그럴 때에만 동치이다.
- 만일 
3. 유효성(validity)
특정 문장을 유효한 문장이라고 할 때가 있습니다. 이때 말하는 '유효한'의 의미는, 모든 모형에서 참인 문장이라는 것입니다. 예를 들어, 
또한 유효한 문장을 동어반복(tautology)라고 말하기도 합니다. 동어반복은 필연적으로 참입니다.
앞에서 배운 논리적 동치라는 개념과 함께 생각해볼까요?
문장 True는 모든 모형에서 언제나 참이므로, 모든 유효한 문장, 동어반복은 True와 논리적 동치입니다.
이러한 개념이 왜 있을까요? 모든 모형에서 참이라는 문장, 즉 유효한 문장은 왜 필요할까요?
그 이유는 간단합니다.
유효한 문장을 통해서 함축의 정의에서 연역 정리(deduction theorem)을 이끌어 낼 수 있기 때문입니다.
연역 정리란,
임의의 문장 
라는 것입니다.
따라서
반대로, 연역 정리는 모든 유효한 함의 문장이 적법한 추리를 서술한다라는 것을 말해 줍니다.
4. 만족 가능성(satisfiability)
마지막으로 알아볼 개념은 만족 가능성(satisfiability) 이라는 것 입니다. 주어진 문장이 참이 되는 모형이 존재하면, 다시말해서 주어진 문장을 만족하는 모형이 존재하면, 그 문장은 만족 가능한 문장입니다. 즉 모든 모형 중에서 하나 이상의 모형이 주어진 문장을 만족했을때 그 문장은 만족 가능하다라고 말합니다.
만족 가능성은 문장을 만족하는 모형이 하나이상 나올 때 까지 모든 가능한 모형들을 확인합니다.
이러한 만족 가능성이라는 개념은 위에서 알아본 유효성 개념과 많은 관계를 가지고 있습니다.
예를 들어, A라는 문장은 오직 not A가 만족 불가능일 때에만 유효한 문장입니다. 또한 그 대우(contrapositive) 또한 역시 참입니다. 이를 바꿔말해서, A라는 문장은 not A가 유효하지 않을 때에만 만족 가능한 문장입니다.
그리고 아래와 같은 관계도 존재합니다.
또한 귀류법은 반박(refutation)에 의한 증명 또는 모순(contradiction)에 의한 증명이라고 부르기도 합니다.
귀류법에서는 일단 문장
이렇게 해서 명제 정리 증명에 앞서 몇가지 세부적인 개념에 대해 알아보았습니다.
다음 포스팅에서는 증명을 이끌어 내는 데 사용할 수 있는 추리규칙들에 대해서 알아보겠습니다.
'AI & BigData > 인공지능 이론' 카테고리의 다른 글
| 인공지능(AI) #6_ 분해(Resolution), 논리곱 표준형(CNF) (2) | 2017.12.09 |
|---|---|
| 인공지능(AI) #5_ 추리 규칙(Inference rule), 단조성(Monotonicity) (0) | 2017.11.20 |
| 인공지능(AI) #3_ 명제 논리와 모형 점검 방식 (0) | 2017.11.05 |
| 인공지능(AI) #2_ 논리, 추론, 모형(logic, entailment, model) (3) | 2017.11.02 |
| 인공지능(AI) #1_ 논리적 에이전트, 지식 기반 에이전트, 웜푸스 세계 (0) | 2017.11.02 |