powered by : https://doorbw.tistory.com/64?category=684964
7.5 Propositional Theorem proving
리는 모든 모형들을 열거하면서 문장이 모든 모형에서 성립하는지 점검하는 모형 점검 방식에 대해 알아보았습니다. 이제는 정리 증명(Theorem proving)을 이용하여 함축 관계를 확인하는 방법에 대해서 알아보겠습니다. 우리가 앞으로 알아볼 접근 방식에서는 주어진 문장의 증명을 구축하여 함축관계를 확인하기 위해서 지식 기지(KB)에 있는 문장들에 여러가지 추리 규칙들을 적용할 것 입니다. 우리가 앞에서 살펴본 모형 점검 방식에 비해, 모형이 많을 수록 또는 정리 증명의 내용이 짧을 수록 보다 효율적인 증명 알고리즘이 될 것입니다.
그리고 먼저, 인사말에서 언급하였듯이 정리 증명 알고리즘의 세부사항에 앞서, 함축과 관련된 몇가지 추가적인 개념을 소개하겠습니다.
Logical equivalence
논리적 동치(Logical equivalence)란, 두 문장 a와 b가 동일한 모형들에서 참일 때, 그 두 문장은 동치관계라고 하는 것 입니다.
유효성
특정 문장을 유효한 문장이라고 할 때가 있습니다. 이때 말하는 '유효한'의 의미는, 모든 모형에서 참인 문장이라는 것입니다.
satisfiability
만족 가능성(satisfiability) 은 주어진 문장이 참이 되는 모형이 존재하면, 다시말해서 주어진 문장을 만족하는 모형이 존재하면, 그 문장은 만족 가능한 문장입니다. 즉 모든 모형 중에서 하나 이상의 모형이 주어진 문장을 만족했을때 그 문장은 만족 가능하다라고 말합니다.
예를 들어, A라는 문장은 오직 not A가 만족 불가능일 때에만 유효한 문장입니다. 또한 그 대우(contrapositive) 또한 역시 참입니다.
오른쪽 수식이만족한다면 왼쪽의 수식이 만족한다는 것을 증명하기 위해 오른쪽 수식의 α로 부터 β를 증명하는 것은 귀류법이며 귀류법은 반박(refutation)에 의한 증명 또는 모순(contradiction)에 의한 증명이라고 부르기도 합니다.
7.5.1 Inference and proofs(추리 규칙과 증명)
증명이라는 것은 어떤 원하는 목표로 향해가는 결론들, 문장들의 사슬입니다.
그러한 증명을 만들어 내는데 사용되는 가장 잘 알려진 규칙은 아래와 같이 표기하는 전건 긍정(Modus Ponens)입니다.
논리곱 소거(AND-elimiation)
또 다른 유용한 추리규칙으로는 논리곱 소거(AND-elimination)이 있습니다.
논리곱으로 주어진 문장에서 임의의 논리곱 성분을 추리할 수 있음을 뜻하며 다음과 같이 표기합니다.
건전한 추리(Sound inference)
전건 긍정과 논리곱 소거 모두 전적으로 건전한 추리임을 알수 있기 때문에, 위에서 알아본 두가지 추리규칙을 통해 전체적인 모형을 열거하지 않고도 건전한 추리를 이끌어 낼 수 있습니다.
단조성(monotonicity)
이는 특정 지식기지에 정보, 문장이 추가된다면 이는 함축된 문장들의 집합이 항상 커지기만을 의미할 뿐이지, 추가된 것에 의해 이미 추리된 결론이나 기타 결론에 영향을 주지 않는다는 것입니다.
즉, 지식 기지에서 추리를 통해 얻어낸 결론 A가 존재할 때, 또 다른 단언 명제 B가 추가된다면 이는 추가적인 결론들을 이끌어내는데 도움이 될 수도 있겠지만, 이미 추리된 결론 A는 무효화되지 않습니다.
단조성을 통해 우리는 지식 기지에서 적절한 전제를 찾았다면 언제라도 추리 규칙들을 적용할 수 있음을 알 수 있습니다.
추리 규칙의 결론은 지식 기지에 있는 또 다른 지식과는 무관하게 옳아야 하기 때문입니다.
7.5.2 Proof by resolution
분해(Resolution)
앞에서 추리규칙들이 건전하다. 올바르다라는 점을 함께 알아보았지만 아직 부족한 한가지는, 그러한 추리규칙들을 사용하는 추리 알고리즘이 완결적인지 알아보지 않았습니다. 여기서 완결적이라는 것은, 해당 알고리즘이 도달 가능한 목표가 존재할 때, 그것을 반드시 찾아낼수 있는가에 대한 것입니다.
따라서 이번에는 분해(Resolution)라는 추리규칙을 알아보는데, 이러한 규칙을 완결적 검색 알고리즘과 함께 사용하면 완결적인 추리 알고리즘이 도출되는 것을 함께 보도록 하겠습니다.
분해규칙에서는 인수분해(factoring)이라는 추가적인 행동이 필요합니다.
인수분해란, 리터럴의 중복된 복사본들을 제거하는 것입니다. 예를 들어 (A v B)를 (A v ~B)로 분해하면 (A v A)가 나오는데 이는 인수분해를 통해 하나의 A로 축약될 수 있습니다.
분해규칙의 건전성은 다른 절의 리터럴 mj에 상보적인 리터럴 li를 생각해보면 쉽게 확인할 수 있습니다.
분해 규칙에서 더 놀라운 사실은, 이것이 완결적인 추리 절차들이 속한 모임의 기저를 형성한다는 점입니다. 분해 기반 정리 증명기는 명제 논리의 임의의 문장 a 와 b에 대해 a|=b의 진리를 결정할 수 있습니다. 분해가 이를 어떻게 달성하는지 함께 알아보겠습니다.
논리곱 표준형(CNF : Conjunctive Normal Form)
분해 규칙은 절에만 적용되는 것을 보았습니다. 즉 절들로 이루어진 지식기지와 질의에만 유관한 것으로 보입니다. 그렇다면 우리는 분해규칙으로 모든 명제 논리를 위한 완결적인 추리 절차를 얻을 수 있을까요?
그 답은, 모든 명제 논리 문장은 절들의 논리곱과 논리적으로 동치라는 것입니다.
절들의 논리곱 형태로 이루어진 문장을 가리켜 우리는 논리곱 표준형(CNF)이라고 합니다.
그럼 문장을 CNF로 변환하는 절차를 함께 보도록 하겠습니다.
-
B11 <=> (P12 v P21) 이라는 문장을 CNF로 변환합니다.
-
<=>을 소거합니다. 즉, a<=>b 를 (a=>b)∧(b=>a) 으로 대체합니다.
(B11 => (P12 v P21)) ∧ ((P12 v P21) => B11) -
=>를 제거합니다. 즉, a=>b를 ~a v b로 대체합니다.
(~B11 v (P12 v P21)) ∧ (~(P12 v P21) v B11) -
CNF에는 ~이 리터럴에만 있어야합니다. 이를 위해 아래의 세개 방식 중 적절한 것을 적용하여 ~을 괄호 안으로 옮깁니다.
지금의 예에서는 세번째 규칙을 한번만 적용하면 됩니다.
(~B11 v P12 v P21) ∧ ((~P12 ∧ ~P21) v B11) -
이제 ∧, v 연산자와 리터럴들로 이루어진 부분들이 중첩된 형태의 문장이 나왔습니다. 이제 분배법칙을 적용해서 v를 ∧에 대해 적절히 분배합니다.
(~B11 v P12 v P21) ∧ (~P12 v B11) ∧ (~P21 v B11)
이렇게 해서 원래의 문장이 세개의 절의 논리곱 형태로 된 CNF로 변환되었습니다.
이전보다 언어로써 표현하기는 힘들지만 완결적인 분해 절차의 입력으로써 사용될 수 있습니다.
분해 알고리즘(Resolution algorithm)
분해 규칙에 기초한 추리 절차들은 이전 포스팅에서 소개드렸던 귀류법(모순에 의한 증명)의 원리를 이용합니다.
즉, (KB∧~a)가 만족 불가능임을 보임으로써 KB|=a가 참임을 증명합니다.
분해 알고리즘은 다음 사진과 같습니다.
위의 알고리즘은 우선 (KB∧~a)를 CNF로 변환합니다. 그리고 그 CNF의 절들에 대해서 분해 규칙을 적용합니다. 상보 리터럴을 담은 각 쌍을 분해해서 제외한다음 새 절을 산출하고 그것을 절들의 집합에 추가합니다. 절들의 집합에는 중복이 허용되지 않습니다. 그러한 과정을 반복하면서 다음 두 조건 중 하나가 만족할 때 결과를 출력합니다.
- 추가할 수 있는 새로운 절이 더이상 없다. 이 경우 KB는 a를 함축하지 않습니다.
- 두 개의 절이 빈 절로 분해된다. 이 경우 KB는 a를 함축한다.
이 때, 빈 절이라는 것은 성분이 하나도 없는 논리합으로써 False와 동치입니다. 즉, (KB∧~a)에 대해 False이기에 KB는 a를 함축하는 것입니다. P와 ~P처럼 서로 상보적인 단위 절을 분해한다면 빈 절이 발생합니다.
그럼 위의 분해 절차를 웜푸스 세계에 적용해 보도록 하겠습니다.
에이전트가 [1,1]에 있을 때에는 미풍을 지각하지 못합니다. 따라서 이웃 칸에는 구덩이가 있을 수 없습니다. 이를 나타내는 지식기지는 다음과 같습니다.
KB = R2 ∧ R4 = (B11 <=> (P12 v P21)) ∧ ~B11
7.5.3 Horn clauses and definite clauses
7.5.4 Forward and backward chaining
전방 연쇄
먼저 전방 연쇄란, 기존의 알려진 사실들로 하여금 새로운 사실을 추리하면서 나아가는 방법입니다. 이름처럼 원래 알고 있는 것을 바탕으로 앞으로 나아가는 방법이죠. 즉, 한 문장, 함의에 대한 모든 전제가 알려져 있는 사실이라면 그것에 대한 결론을 새로운 사실로써 지식기지에 추가합니다.
예를 들어, A라는 사실과 B라는 사실을 알고 있을 때, 지식기지에 A∧B=>C 가 있다면 C를 하나의 사실로써 추가할 수 있습니다.
이러한 과정을 통해 알고자 하는 사실 Q에 도달하거나 더 이상 추리가 불가능 할때 까지 반복합니다.
아래의 알고리즘을 살펴보면 전방연쇄가 선형시간으로 실행되는 것을 확인할 수 있습니다.
전방연쇄는 위에서 언급한 바와 같이 진행되며 이를 보면 연역법과 비슷하다는 것을 알 수 있습니다.
이러한 전방연쇄는 건전하며 완결적입니다.
전방연쇄가 건전하다는 것은 쉽게 확인할 수 있는데, 모든 추리는 본질적으로 전건 긍정의 적용이기 때문입니다.
그리고 함축된 원자적 문장들이 모두 유도되기 때문에 완결적임을 알 수 있습니다.
전방연쇄를 아래 그림을 통해 확인하면 보다 쉽게 이해할 수 있습니다.
위의 그림에서 알려진 사실들은 A와 B입니다. 그리고 그래프는 AND-OR 그래프로써 여러 링크가 하나의 호로써 결합된 것은 AND, 논리곱을 의미하며 여러 링크가 호 없이 결합된 것은 OR, 논리합을 의미합니다. 논리곱을 증명하기 위해서는 연결된 모든 링크가 증명해야 하며 논리합에 대해서는 최소 하나의 링크가 참일때 참을 알 수 있습니다.
그림에 대한 이해를 해본다면, 먼저 알려진 사실 A와 B를 통해 A∧B=>L 에서 L이라는 사실을 추가합니다. 그리고 B∧L=>M
을 통해 M이라는 사실을 추가하고 이어서 L∧M=>P를 통해서 P라는 사실을 추가합니다. 그리고 P=>Q를 통해 Q라는 사실 또한 추가할 수 있습니다.
후방 연쇄
이번에는 후방 연쇄(Backward chaining)에 대해서 알아보겠습니다. 후방연쇄는 그 단어에서도 알 수 있듯이 먼저 확인하고자 하는 사실 Q로부터 시작하여 Q를 사실로써 추가하기 위해 지식기지에서 결론이 Q인 함의, 문장을 찾습니다.
예를 들어, Q라는 사실을 확인하고자 하고 지식 기지에 M∧N=>Q 이 있다면 이제 우리는 각각 M, N에 대해서 동일하게 후방 연쇄를 진행합니다. 그리고 원래 알고 있던 사실, A와 B에 도달 했을 때 그 반복을 멈추게 됩니다.
전방연쇄에서 사용되었던 예시를 통해 후방 연쇄의 과정을 살펴보겠습니다.
먼저 Q라는 사실을 확인하려고 합니다. 지식기지에 P=>Q가 있으므로 우리는 P에 대한 후방연쇄를 진행합니다.
그리고 지식기지에 L∧M=>P가 있으므로 다시 L와 M에 대해서 후방연쇄를 진행합니다.
먼저 L에 대해서 진행하면, 지식기지에 A∧P=>L과 A∧B=>L이 있습니다. 이때 A와 B는 우리가 미리 알고있는 사실이기 때문에 L에 대한 후방연쇄는 A∧B=>L을 통해서 증명됩니다.
그리고 이제 M에 대해서 후방연쇄를 진행하면, 지식기지에서 B∧L=>M을 확인하고 B는 우리가 이미 알고 있는 사실이며 L은 방금 위에서 후방연쇄를 통해 추가된 사실이기 때문에 M 또한 후방연쇄를 통해 사실로써 추가합니다.
그럼 다시 L∧M=>P가 후방연쇄를 통해 P가 사실로써 추가될 수 있으며, P=>Q 또한 후방연쇄를 통해 증명되었기에 Q를 사실로써 추가할 수 있습니다.
이러한 후방 연쇄의 효율적인 구현은 선형 시간으로 전방 연쇄와 같습니다.
헌데 후방 연쇄는, 목표 지향적 추론(goal-directed reasoning)의 한 형태로써 종종 후방 연쇄의 비용이 지식 기지 크기의 선형적인 시간보다 훨씬 적을 수 있습니다. 그 이유는, 후방 연쇄가 추론 과정에서 오직 유관한 사실들만 확인하기 때문입니다.
