논리 언어에는 여러 종류가 있지만 가장 기본적인 언어는 명제 논리(Propositional logic)이다. 이보다 표현의 범위가 뛰어난(?) 혹은 넓은 언어가 서술 논리(Predicate Logic)이다.
사용 연산자는 다음과 같다.
t : true
f : false
┐A : not A (negation)
A ∧ B : A and B (conjunction) 논리곱
A ∨ B : A or B (disjunction) 논리합
A ⇒ B : if A then B (implication) A가 참이면 B도 참. - 함축
A ⇔ B : A if and only if B (equivalence) A가 참이면 B도 참, B가 참이면 A도 참
implication과 equivalence도 역시 not, and, or 만 있으면 다 표현할 수 있다.
A ∧ B 와 같은 문장(Formula)을 참이냐 거짓이냐를 판단하는 것을 Semantics(의미론)이라고 할 수 있다.
Semantics은 수학적으로 다음과 같이 정의한다.
Proposition variable을 {참, 거짓}으로 매핑 해주는 함수를 I(Interpretation 혹은 World)라고 부른다. 만약에 Proposition variable(atomic formula)가 n개 존재한다면 Interpretation(World)는 2^n개를 생각해볼 수 있다.
그럼 Interpretation의 참, 거짓이 결정되면, 즉 mapping 함수 I가 결정되면 compound formula, 즉 논리연산자를 이용하여 표현되는 formula의 참, 거짓을 정의하는 것이다.
ex)
I(A ∨ B)는 A가 true이거나 B가 true이면 Interpretation는 true가 된다.
즉 I(A ∨ B) = t iff(if and only if) I(A)=t or I(B)=t이다.
참고로 iff는 수학적으로 양방향적인 의미이며 a iff b를 증명하려면 a가 참이면 b도 참, b가 참이면 a도 참이라는 것을 모두 증명해야 한다.
I(A ⇒ B)는 I(A) = t이고 I(B) = f일 때만 false이다. 이를 수식으로 표현하면 ┐A∨ B가 된다.
이 경우를 이해하기 조금 어려울 수도 있는데 이를 문장으로 바꿔보자.
A : 휴대폰 배터리가 방전되었다.
B : 휴대폰이 켜지지 않는다.
1. A = true, B = true
휴대폰이 방전되었고 휴대폰이 켜지지 않는다.
-> 모순이 없다.
2. A = true, B = false
휴대폰이 방전되었고 휴대폰이 켜진다.
-> 논리적으로 모순이다.
3. A = false, B = true
휴대폰이 방전되지 않았는데 휴대폰이 켜지지 않는다.
-> 모순이 없다. (다른 이유로 켜지지 않을 수 있기 때문이다.)
4. A = false, B = false
휴대폰이 방전되지 않았는데 휴대폰이 켜진다.
-> 모순이 없다.
A ⇒ B, 즉 ┐A∨ B를 도식화하면 다음과 같다.
즉 "가정이 거짓이면 결론은 참이 될 수 있다"라고 보면 된다.
또한 다음과 같은 용어가 있다.
A formula가 satisfiable하다면 이는 최소한 1개 이상의 true interpretation이 존재한다는 것이다. 즉 unsatisfiable하다면 모든 interpretation이 false이다.
만약 모든 interpretation가 true이면 이를 valid하다고 또한 tautologies라고 부른다.
어떤 formula를 satisfiable하는 interpretation을 그 formula의 Model이라고 부른다.
-> Valid한 formula의 negation은 unsatisfiable이다. Valid하진 않지만 satisfiable한 formula의 negation 역시 satisfiable하지만 not valid하다.
ex)
formula A와 B가 있다.
1. A가 satisfiable 한가? -> I(A) = t가 있을 수 있으므로 satisfiable하다.
2. ┐A ∧ A satisfiable 한가? I(┐A ∧ A)=t를 생각할 수 없으므로 답은 no이다.
3. ┐A ∧ A unsatisfiable 한가? 모든 interpretation에서 f이므로 unsatisfiable하다. 즉 모순(contradiction)이다.
4. ┐A ∨ A valid 한가? I(┐A ∨ A) = t이므로 valid(tatologies)하다.
주어진 지식으로부터 새로운 지식이 참으로 유도되는 것을 보여주는 것을 Proof System이라고 하며 Proof System을 설명하기 위해 Entailment(함의), Derivation(유도)가 사용된다.
용어 설명
Entailment : Knowledge Base(KB)로부터 formula Q가 유도(함의) 될까(할까)? 이를 KB |= Q라고 쓰는데 말이 어렵다. 집합(formula) KB에 속하는 모든 Interpretation에서 참일 때 어떤 formula Q의 I(Q)도 참이라면 KB는 Q를 Entails 한다고 한다. 그래도 어려워서 한번 더 반복하면 주어진 지식이 참이면, 즉 그 지식이 참이 되는 모든 Interpretation(World)에서 참이 되는 지식과의 관계를 Entails 하다고 표현할 수 있다.
예를들어서 KB가 A ∧ B이면 "KB entails A"(A from KB)이고 KB |= A라고 쓴다.
그렇다면 KB = {A, ┐A ∧ B} 일 때 KB |= B 인가?
증명 : A가 true이기 때문에 ┐A는 false이다. 그럼 B는 반드시 true이어야 ┐A ∧ B가 true가 된다.
Deduction Theorem
논리식들 F1, …, Fn과 논리식 G가 주어졌을 때, 만약 논리식 (F1…Fn→G)가 유효식이라면, G는 F1…Fn의 논리적 귀결이 된다는 정리이다.
A |= B iff |= A ⇒ B를 증명해보자.
증명
만약 A |= B가 참이면 entailent의 정리에 의해 formula A가 참인 모든 Interpretation에서 B도 참이 된다. 따라서 formula A ⇒ B가 valid가 된다. 왜냐하면 Theorem에 의해 A ⇒ B는 ┐A ∨ B인데 A가 참이면 B도 참이므로 ┐A ∨ B는 항상 참이된다. 또한 A가 거짓이면 ┐A ∨ B는 당연히 참이다.
반대방향으로 우측의 |= A ⇒ B가 참이면 모든 Interpretation에서 A ⇒ B가 참이 된다. 그러므로 A가 참인 모든 Interpretation에서 B도 참이다. 따라서 entailment 정의에 의해 A |= B는 참이다.
Contradiction Theorem
A |= B iff |= A ⇒ B
Deduction Theorem에 의해 KB |= A이 참이면 KB ⇒ B가 valid(tautology)가 된다.
그리고 KB ⇒ A ≡ ┐KB ∨ A되고 tautology를 부정해보자.
즉 ┐(┐KB ∨ A) ≡ ┐(┐KB ∨ A) ≡ KB ∧ ┐A는 unsatisfiable(contradiction)이 된다.
모순이 발생했으므로 A |= B iff |= A ⇒ B는 참이다.
KB에 증명하려는 formula A를 부정하여 KB에 추가(확장)하고 추가된 KB가 contradiction이 됨을 증명하면 KB로부터 A가 유도되는 것이 증명된다.
즉 KB |= Q if and only if KB ∧ ┐Q is unsatisfiable을 증명하려면 Q를 부정해서 KB를 확장하고 이게 모순인 것을 밝히면 된다는 것이다.
Proof by Contradiction Theorem은 무언가 멋있어보이는 증명 방법이다.
위에서 증명한 KB = {A, ┐A ∧ B} 일 때 KB |= B 인지를 Contradiction Theorem으로 증명해보자.
증명 : B를 부정해서 ┐B를 KB에 추가하면 KB = {A, ┐A ∧ B, ┐B}가 된다. 이는 ┐A ∧ B가 true이므로 B도 true이다. 그럼 ┐B와 B가 모두 true인 모순이므로 KB |= B가 된다.
용어 설명
Derivation: Entailment를 증명하는 방법은 보통 KB에 있는 formula로부터 어떤 규칙을 적용해서 다음 formula를 유도(derive)하게 되고 궁극적으로 증명하는 formula가 나오도록 하는 프로세스로 패턴 매치 과정이라고 볼 수 있다. 이러한 과정을 Derivation이라고 하고 KB |- A라고 쓰며 formula A가 KB로 부터 derive되었다고 한다.
예를들어서 formula A1로부터 A1 -> A2 -> A3 ... -> An formula An이 유도되는 과정을 derivation이라고 한다.
Syntactic derivation and semantics entailment
만약 KB로부터 임의의 formula A가 derive하는지 증명하는 프로그램(Theorem Prover) p가 있다고 하자. 만약 p가 참이라고 증명하면 KB |= A라고 하자. 이런 경우 p를 sound하다고 한다. 하지만 p가 모든 참인 formula를 증명하는 것도 중요하다. 만약 모든 참인 formula를 증명한다면 이를 Complete하다고 부른다.
만약 KB |= A일 경우 프로그램 p도 참이라면 KB |- A이면 프로그램 p를 Complete하다고 한다. 하지만 Theorem Prover가 Complete해서도 충분하지 않다. 왜냐하면 거짓인 formula를 참이라고 하면 Sound하지 않기 때문이다. 따라서 Sound and Complete Theorem Prover가 가장 적절하다고 할 수 있다.
ex)
KB |= Q iff KB |- Q 하는 p가 존재하는가? 있다. (대표적으로 truth table이다.)
(왼쪽은 entailmment이고 오른쪽은 derivation이다.)
이러한 Sound & Complete Theorem Prover를 만드는 방법으로 Resolution이라는 inference rule이 있다. 이러한 inference rule을 적용하기 위해선 formula를 표준화된 형태인 CNF(Conjunctive Normal Form) formula로 바꿔야한다.
CNF란? not, and, or로만 이루어진 형태이다.
ex) (┐A ∧ B) ∨ (C ∨ B) ∧ D
inference rule중에 Modus Ponens Rule이 있다.
Modus Ponens Rule이란?
서술 논리문의 wff들로 이루어진 집합에 적용되어 새로운 wff를 생성할 수 있는 추론 규칙의 일종으로, 두 개의 wff를 w1과 w1→w2가 있을 때 이들로부터 새로운 wff, w2를 생성하는 규칙이다.
이때문에 조금 더 일반화(?) 된 Resolution Rule을 사용하는데 다음과 같다.
Resolution inference rule은 sound 하지만 complete 하지는 않다. 그러나 Proof-by-Contradiction을 이용하면 sound하고 complete한 Theorem Prover를 만들 수 있다.
예를 들어보자. 다음과 같이 모두 true인 Formula가 있다. (S, N, P)
이를 CNF하면 다음과 같다.
이제 resolution proof을 해서 결과를 얻어내자.
만약 (┐S)는 참이 될 수 있을까?
증명하기 위해 명제를 부정하여 S 를 만들고 KB에 추가하면 기존에 있던 (┐S)2에 의해 모순이 발생한다. 즉 참이 될 수 없다. (참은 ┐S ∧ N ∧ P 만 될 수 있다.)
한가지 예를 들어서 참인지 거짓인지 밝혀보자.
formalization을 해서 Q를 얻어내면 위와 같다. 이제 ┐Q가 unsatisfiable한 것만 보이면 된다.
CNF를 하여 증명하면 결국 마지막에 ()가 되고 contradiction이 되었다. 즉 ┐Q가 unsatisfiable한 것이다.
Resolution을 하면 복잡해서 오래걸린다. 조금 더 현실적으로 하기 위해 명제논리를 약간 제한하는 것을 Horn clauses라고 한다.
Horn clauses는 많아봐야 positive literal은 1개이거나 없는 형태의 formula이다.
왜 필요한가?
"만약에 날씨가 좋고 눈이 오면 나는 스키를 타러 가거나 일을 할거야"는 모호한 이야기이다. 이를 "만약에 날씨가 좋고 눈이 내리면 나는 스키를 타러 갈거야"는 모호한 표현이 아니게 된다. 이처럼 Horn clauses는 명확하게 해주는 것이다. CNF를 이렇게 제한한다면 매우 효율적이게 된다.
A1 ∧ A2 ∧ ... ∧ An ⇒ B 일 때 왼쪽을 antecedent, 오른쪽을 consequent로 구분한다. 그런데 오른쪽에 존재하는 positive formula B를 head라고 부른다.
여기서 A1 ∧ A2 ∧ ... ∧ An ⇒ B ≡ ┐A1 ∨ ┐A2 ∨ ... ∨ ┐An ∨ B 이므로 Horn clause이다. 만약 B 대신 f가 있어도 positive literal이 0개인 Horn clause이다. 단순히 B 형태 즉 1개의 positive literal은 fact라고 부른다.
Horn clauses 예를 들어보자.
KB를 정의하면 다음과 같다.
그럼 skiing을 타러 가는건지를 증명하려면 ┐(skiing)0 을 가정하자.
그럼 (skiing)6과 ┐(skiing)0에 의해 MP(0,6)이 contradiction이 발생한다.
즉 스키를 타러 가는 것이다.
또한 SLD resolution(for horn clauses)를 사용하면 아주 효율적이다.
SLD란 Selection rule driven linear resolution for definite clauses이다.
즉 다음 단계에서 전단계 결과를 resoultion하기 때문에 아주 빠르게 계산할 수 있다.
정리하고보니 참조를 많이 했지만 설명이 어려워보인다. 나도 쓰면서 직접 계산을 하면서 하면 이해가 되지만 귀찮은 이유로 머리속에서 생각을 하면서 쓰면 이해가 잘 안간다. 확실히 어려운 주제이고 내용이 어렵다.
어찌됐든 이번 포스팅에서는 명제 논리(Propositional logic)에 대해서 다뤘는데 다음 포스팅에서는 서술논리에 대해서 정리하도록 하겠다.
- 참고
아주대학교 정보통신대학원 인공지능(Artificial Intelligence(김민구 교수님))의 강의를 수강하며 배운 내용을 바탕으로 정리하였습니다. 그리고 강의 내용은 ertel's slide가 참고 되었습니다. 학습 목적으로 포스팅 합니다.
도움이 많이 됐습니다. 감사합니다.
답글삭제