명제논리

* Symbolic (Knowledge) Representation

인공지능 분야에서 지식을 표현하기 위한 방법 중 문법과 의미가 수학적으로 잘 정의된 언어는 논리 (Logic)라는 언어이다. 논리 언어는 여러 종류가 있지만 가장 간단하고 기본적인 언어는 명제 논리 (Proposition) 이다. 이 보다 표현 능력이 뛰어난 논리 언어가 서술 논리 (Predicate) 이다 .
 

서술 논리의 표현 능력은 명제 논리의 능력을 포함하는 강력한 언어이다.

서술 논리는 1차 서술 논리 (First-order Predicate Logic) 혹은 단순히 1차 논리라 부르기도 한다.

서술 논리 이외에서 다른 변형의 논리, 예를 들어 Modal Logic, Fuzzy Logic, Probabilistic Logic 등이 있지만 서술 논리의 이론을 크게 벋어나지 못한다고 할 수 있다. 또한 High-order Logic (2차, 3차... Logic)이 있지만 수학적인 의미론이 잘 정립되지 못한다고 할 수 있어, 1차 서술 논리가 현재로써는 가장 문법과 의미론이 잘 정립된 언어라고 해도 틀린말이 아니다.

 

* A very Simple Knowledge Representation Language: Propositional Logic
 - We read the symbols and perators in the following way:
   · t:  "true"
   · f:  "false"

   · ¬A: "not A" (negation)
   · A∧B: "A and B" (conjunction)
   · A∨B: "A or B" (disjuntion)
   · A⇒B: "if A then B" (implication)
   · A⇔B: "A if and only if B" (equivalence)

 

기본적인 명제 논리에서 사용되는 논리 연산자는 disjunction ∨ (혹은 or ) 와 conjuction ∧ (혹은 and) negation ¬ (혹은 not) 의 연산자가 사용되는데 위 정의에서 ⇒ (implication) 와 ⇔ (equivalence) 추가되었다.

하지만 A⇒B는 ¬A∨B와 동일한 의미로 표현되고 A⇔B는 (A⇒B)∧(B⇒A)로 동일한 의미로 표현 가능하나 편의상 추가하였다.

 

 Example 1.

> 명제 논리에서 formula (문장)의 정의가 재귀적 (Recursive)하게 되어 있다. 위 예에서 사용되고 있는 것 중에 예를 들어, formula^formula도 formula이어서 A∧A∧A도 문법적으로 맞는 formula가 된다. 같은 원리로 (¬A∧B)⇒(¬C∨A)도 formula가 되는 것이다. 

> (((A))∨B)도 맞는 formula이지만 필요에 따라 괄호를 생략하여 간략하게 A∨B로 표현할 수 있다.

 

 

* Semantics (의미론)
논리에서의 의미론은 문장, 즉 formula가 참이 되는가 거짓이 되는지를 정하는 것이다.
따라서 명제 논리에서 의미론은 문법적으로 맞는 formula의 참과 거짓을 정하는 함수 (mapping)를 정의하는 것으로 부터 출발한다.

Mapping 함수 I, 즉 Interpretation (혹은 assignment)는 모든 proposition (formula)의 truth 값 (참(t) 또는 거짓(f))을 지정한다. 하나의 세상이 이러한 Interpretation에 의하여 모든 propositon들의 참값이 결정되므로 이 함수를 world라고 부르기도 한다.

따라서 시그마에 들어있는 proposition variable의 수가 n이면 2^n 가지의 interpretation (world)을 생각할 수 있다.

 

 

* Semantics of Propositional Logic
명제 논리의 의미론은 시그마에 들어 있는 모든 proposition variable (atomic formula) 참값 (t or f)이 결정되면, 즉 mapping 함수 I가 결정되면 atomic formula가 아닌 compound formula, 즉 논리 연산자 ∨, ∧, ¬, ⇒, ⇔를 이용하여 표현되는 formula의 참값을 정의하는 것이다.

예를 들어 AvB의 참값, 즉 I(AvB)값은 I(A)가 참(t)이거나 I(B)가 참이면 참이 된다. 즉 I(A∨B) = t iff(if and only if) I(A)=t 또는 I(B)=t이다. 주의 iff는 수학적으로 양방적인 의미이다. 예를 들어 s iff t라는 말은 s가 참이면 t도 참이고, t가 참이면 s도 참이라는 뜻으로  이 것(s iff t)을 증명하려면 양방향으로 모두 증명을 해야한다.

명제 논리에서 의미론을 정의하려면 문법에서 정의한 모든 formula의 정의에 대하여 참값을 정의하여야 (위에서 예로 A∨B 참값을 정의한 것 처럼)한다.

이를 간편하게 표현하려면 진리표 (Truth Table)로 모든 formula의 참값을 정의한다.

 

 

* Truth Table

 Example 2.

> 위 정의에서 empty formula 는 항상 참 ( 인 formula 로 정의하고 있다 . Atomic formula t 와 같다

> A⇒B의 참값 즉 의미론의 정의를 생각보면, I(A⇒B)의 값은 I(A)=t이고 I(B)=f 일 때만 f이고 나머지 경우는 모두 t이다.

즉, I(¬A∨B)=f이고 나머지 경우는 모두 t가 된다고 할 수 있다. 따라서 A=>B iff ¬A∨B가 성립함을 알 수 있다. 

 

 Example 3.

 Definition: Two formulas F and G are called semantically equivalent if they take on the same truth value for all interpretations. We write F ≡ G.

 

> F와 G가 논리적으로 같다는 말은 모든 Interpretation (혹은 world)에서 그 참값이 같다는 말이다. 이를 F≡G라고 표현하였다. 물론 여기서 ≡는 논리적 연산자가 아니므로 F≡G는 formula가 아니다. 다만 두 formula F와 G의 참값이 같다는 관계를 표현한 것이다. 이러한 관계를 논리 연산자를 이용하여 F⇔G 표현하면 명제 논리 문법에 따라 이 식도 formula가 된다.

> 즉, 논리 언어를 목적 언어 (Object Language)라고 하면 F⇔G는 논리 언어 즉 목적 언어로 표현된 formula이지만, 목적 언어를 설명하기 위해 사용하는 언어 (자연어)를 메타 언어라고 한다. 따라서 F≡G 메타 언어로 두 formula의 관계 (참값이 동일하다는) 표현했다고 할 수 있다.

 

* Satisfiability

- satisfiable: if it is true for at least one interpretation.

- logically vaild or simply vaild: if it is ture for all interpretatinos. True formulas are also called tautologies.

- unsatisfiable: if it is not true for any interpretation

Formula가 몇개의 Interpretation(World)에서 참이냐 거짓이냐에 따라 그 formula를 다음의 몇개의 클래스로 나누어 부를 수 있다.

  · 만약 formula가 최소한 하나의 Interpretation에서 참이면 그 formula를 satisfiable하다고 부른다.
  · 만약 formula가 모든 Interpretation에서 참이면 그 formula를 valid(또는 logically valid)라고 부른다. 이렇게 항상 참인 formula를 tautology라고 말한다.

    예를 들어 "산은 산이요, 물은 물이다." 명제 논리의 formula로는 A∨¬A가 tautology이다.
  · 만약 formula가 모든 Interpretation에서 거짓이면 그 formula를 unsatisfiable 하다고 부른다. 즉 참인 Interpretation이 하나도 없을 경우를 말한다.

  · 어떤 formula를 satisfiable하는 Interpretation을 그 formula의 모델이라고 부른다.  

 

 Example 4.

 Let 𝐴 and 𝐵 formulas.

 

 1. Is 𝐴 is satisfiable ?

  > 물론 I(A) = t 인 Interpretation 을 생각할 수 있으므로 satisfiable 하다.

 2. Is ¬𝐴∧𝐴satisfiable ?

  > I(¬𝐴∧𝐴) = t 를 생각할 수 없다 . 답은 No.
  > unsatisfiable ? ( 모든 Interpretation I 에서 I ¬𝐴 𝐴) = f 이다 . 그러므로 unsatisfiable , 즉 contradiction)

 3. Is ¬𝐴∨𝐴valid? 

  > 모든 Interpretation I 에서 I ¬𝐴∨𝐴) = t 이다 . 그러므로 valid(tautology) 이다

 

 

* Theorems

The operations ∧, ∨ are commutative and associcative, and the following equivalences are generally valid:

> 앞에서 언급한 formula 들은 모두 valid 하다 . 즉 모든 interpretation 에서 각 formula 는 참의 값을 갖는다 .이러한 formula 들이 참인지 아닌지 증명하는 시스템을 Proof System 이라고 한다 . 또한 항상 참인 즉 (valid) formula 를 정리 (Theorem)라고 한다.

 

 

* Entailment (함의)

Definition: A formula KB entails a formula Q (or Q follows from KB) if every model of KB is also a model of Q. We write KB |= Q

Entailment는 중요한 정의로 주어진 지식(formula)로 부터 어떤 지식(formula)이 유도되는 것에 대한 정의이다. 다시 말하면 주어진 지식이 참이면, 즉 그 지식이 참이 되는 모든 Interpretation(World)에서 참이 되는 지식(formula)과의 관계를 Entailment라고 한다.

예를 들어 KB가 A∧B면 "KB entails A"라고 말할 수 있으며, KB |= A라고 쓴다. 물론 우리는 entailment의 정의에 의하여 혹은 진리표를 작성해서 이러한 선언이 참인 것을 증명할 수 있다.

KB(Knowledge Base)는 또한 formula들을 집합으로 볼 수도 있다. 왜냐하면, 집합에 속한 각 formula들의 conjunction으로 하는 KB를 formula로 볼 수 있기 때문이다.

 

 Example 5.

 Let 𝐾𝐵={𝐴,¬𝐴∨𝐵}. 𝐾𝐵╞ 𝐵? How can we prove it?
 

 > 간단한 Theorem Prover로 진리표에 의한 증명 방법이 있으나, 이런 방법은 proprosition variable이 n개 있을 경우 2^n의 시간이 걸린다는 비효율성 문제가 있다. 따라서 resolution이라는 방법을 사용하여 효율적으로 처리하는 것이 바람직하다.

 

 > 𝐼에서 𝐴∧(¬𝐴∨𝐵)이  true 이므로, A는 true이고 ¬𝐴∨𝐵도 true 이다.

𝐼에서 A는 true이기 때문에 ¬𝐴는 false이다. 그러므로 𝐵가 반드시 true 이여야만 ¬𝐴∨𝐵는 true가 성립된다.

 

 

* A Simple Architecture of Knowledge Based System
보통 지식기반 시스템(Knowledge Based System)의 모듈은 간단하게 2가지로 구성되어 있다. 지식베이스(KB)와 추론 기능을 담당하는 추론엔진(Interence Engine)으로 구성되어 있다. 물론 그 외에서 학습 모듈, 설명해 주는 모듈, 인터페이스 등 많은 모듈이 포함될 수 있다.

KB는 개념적으로 지식(formula)의 집합으로 볼 수 있으며, Interence Engine은 사용자의 요청에 따라 크게 다음 2가지의 기능을 담당한다. 1) 사용자가 지식을 말하면 (Tell) 지식을 KB에 넣는 작업, 2) 사용자가 질문을 하면(Ask) 질문에 답하는 업무

Tell은 때로는 Assert(주장하다)라는 용어를 사용하기도 한다. Ask는 주어진 지식이 참인지 거짓인지에 대한 답을 주는 것이 보통이다. 다시 말하면 KB로 부터 주어진 지식이 Entailment 되는지를 알아내야 하는 것이다. 따라서 이를 위해 Theorem Prover가 필요한 것이다.

 

* Deduction Theorem (연역 정리)
 - Theorem
   (Deduction theorem)
   A |= B if and only if |= A⇒B

   => The truth table method is a proof system for propositional logic !
   => Disadvantage: very large computing time in the worst case (2^n interpretations).

   If a formula KB entails a formula Q, then by the deduction theorem KB=>Q is a tautology.

   Therefore the negation ¬(KB=>Q) is unsatisfiable.

   We have: ¬(KB⇒Q) ≡ ¬(¬KB∨Q) ≡ KB∧¬Q

 

 Example 6. 

 (Deduction theorem)
 A |= B if and only if |= A⇒B

 

> 위의  A |= B if and only if |= A⇒B (deduction theorem )은 매우 중요한 theorem 이다 . 이 정리에서 우편에 있는 statement 인 ╞ A ⇒ B 는 entailment ( ╞ 의 오른쪽에 지식베이스가 공집합 (empty 인 것을 알 수 있다 . 이는 지식이 없어도 A ⇒ B 은 참 , 즉 valid(tautology) formula 라는 뜻이다 . 따라서 만약에 좌편의 statement 인 A ╞ B 가 참이면 우편의 statement 인 ╞ A ⇒ B 가 참이고 즉 A ⇒ B 가 tautology 이고 , 또 반대로 우편이 참이면 좌편이 참이 된다 . 이를 증명하기 위하여는 다음과 같이 양방향으로 증명을 해야 한다 .

 

> 만약 A ╞ B 가 참이면 entailment 의 정의에 의하여 formula A 가 참인 모든 Interpretation 에서 B 도 참이 된다 따라서 formula A ⇒ B 가 항상 참인 valid formula 가 된다 . 왜냐하면 Theorem 에 의하여 A ⇒ B 는 ¬𝐴∨𝐵인데 , A 가 참이면 B 도 참이므로 ¬𝐴∨𝐵는 항상 참이다 또한 A 가 거짓이면 ¬𝐴∨𝐵는 당연히 참이다 . 반대 방향으로 우편의 statement ╞ A ⇒ B 가 참이면 모든 Interpretation 에서 A ⇒ B 가 참이 된다 . 그러므로 A 가 참인 모든 Interpretation 에서 B 도 참이다. 따라서 entailment 정의에 의하여 A ╞ B 는 참이다.
    

* proof by contradiction

Deduction theorem에 의하여 KB |= A가 참이면 KB⇒A가 valid(tautology)가 된다. 그런데 KB⇒A ≡ ¬KB∨A가 된다. Tautology를 부정하면, 즉 ¬(¬KB∨A) ≡ KB∧¬A는 unsatisfiable (즉 contradiction)이 된다.

지식베이스 KB에 증명하려는 formula A를 부정하여 즉 ¬A를 KB에 추가하고 추가된 지식베이스가 contradiction이 됨을 증명하면 KB로 부터 A가 유도되는 것이 증명된다. 이러한 증명 방법이 다음 정리로 Proof by Contradiction이다.

 

 Example 7. 

 (proof by contradiction)
 KB |= Q if and only if KB∧¬Q is unsatisfiable.

 

  · We want to prove KB |= B.
  · KB = {A, A⇒B}
  · KB U {¬B} = {A, A⇒B, ~B} = {A, ¬A∨B, ¬B}

 

 > Assume that every formulas in KB is true. Since A and ¬A∨B are true, B is true.

Therefore, there is acontradiction in KB U {¬B}. Q.E.D.

 

 

* Derivation 

Entailment를 증명하는 방법은 보통 KB에 있는 formula로부터 어떤 규칙을 적용해서 다음 formula를 유도(derive)하게 되고 궁극적으로 증명하는 formula가 나오도록 하는 프로세스로 패턴 매치 과정이라고 볼 수 있다. 이러한 과정을 Derivation이라고 하고 KB |- A라고 쓰며 formula A가 KB로 부터 derive되었다고 한다.

예를들어서 formula A1로부터 A1 -> A2 -> A3 ... -> An formula An이 유도되는 과정을 derivation이라고 한다.

 

만약 derive 하는 프로그램 (Theorem p 를 명시하여 프로그램 p 가 formula A 를 KB 로부터 derive 하였다고 말하면 다음과 같이 쓴다 : KB┣ p A.

 

 

* Syntactic derivation and semantics entailment
 - KB |= Q if and only if KB |- Q?
  (entailment)             (derivation)

 => The answer: Yes in propositional logic.
 => There exists a sound and complete theorem prover

 

 - The theorem prover is sound
   if KB |- Q then KB |= Q.
 - The theorem prover is complete
   if KB |= Q then KB |- Q. 

 

만약 지식베이스 KB 로부터 임의 formula A 가 derive 하는지 증명하는 프로그램 (Theorem Prover) p 가 있다고 하자 . 만약 프로그램 p 가 참이라고 증명하기만 하면 A 가 KB 로부터 정말 entail 된다고 하자 . 이런 경우 프로그램 p 를 Sound 하다고 한다 . 다시 말하면 만약 KB┣ p A 일때 KB ╞ A 일 경우 프로그램 p 를 Sound 하다고 한다 . 그러나 , Theorem Prover p 가 sound 한 것으로는 충분치 않다 . 왜냐하면 프로그램 p 가 모든 참인 formula 를 증명하는 것도 중요하기 때문이다.

 

만약 프로그램 p 가 모든 참인 formula 를 증명할 수 있다면 이런 Theorem Prover p 를 Complete 하다고 부른다 . 다시 말하면 , 만약 KB ╞ A 일 경우 프로그램 p 도 참이라고 하면 즉 , KB┣ p 이면 프로그램 p 를 Complete 하다고 한다 . Theorem Prover 가 Complete 만 해서도 충분치 않다 . 왜냐하면 거짓인 formula 를 참이라 하면 Sound 하지 않기
때문이다 . 따라서 , Sound and Complete Theorem Prover 가 가장 좋은 것이다.

Sound & Complete한 Theorem Prover를 만드는 방법으로 Resolution이라는 inference rule이 있다. 
이러한 inference rule을 적용하기 위하여 임의의 formula를 표준화된 형태인 CNF(Conjunctive Normal Form) formula로 바꿀 필요가 있다. 

 

 

* Definition of CNF (conjunctive normal form)

논리곱 표준형(conjunctive normal form)은 절의 논리곱으로 나타낸 논리식을 말한다. 여기서 절은 리터럴의 논리합으로 이루어진다. 논리곱 표준형의 영문 표기를 줄여서 CNF라고도 한다.

 

CNF와 반대로 리터럴의 논리곱으로 이루어진 절들을 논리합으로 연결할 수도 있다. 이를 논리합 표준형이라고 한다.

모든 명제 논리식은 동등한 CNF로 변환될 수 있다. 이 변환은 이중부정 법칙, 드모르간 법칙, 분배 법칙 등을 써서 이루어진다.

 

리터럴의 개수가 3개 이하로 제한된 CNF를 3-CNF라고 하며 계산 이론에서 중요하게 다루어진다. 다른 개수로 제한할 때도 마찬가지로 정의할 수 있으나 2-CNF, 3-CNF 이외에는 중요하게 다루지 않는다.

> CNF는 not, and, or로 이루어진 형태이다.

 

 

* Proof calculus (inference rule)
 => Modus ponens is sound but not complete.

 

-  sound

   · 어떤 명제가 증명이 가능하면 그 명제는 반드시 참이다. (성립)

   · 어떤 명제가 참이라면 그 명제는 반드시 증명이 가능하다. (미성립)

- complete

   ·  어떤 명제가 증명이 가능하면 그 명제는 반드시 참이다. (성립)

   ·  어떤 명제가 참이라면 그 명제는 반드시 증명이 가능하다. (성립)

 

 Example 8.

 Counter Example: Let KB 𝐴⇒𝐵,𝐴∨𝐵}. 𝐾𝐵╞𝐵

> In this example, formula B is entailed from KB, because if A is true then B is true by Modus Ponens and if A is false then B is true since 𝐴

𝐵 is true. But using only Modus Ponens inference rule, we can not prove 𝐾𝐵╞𝐵.

  
앞의 Theorem에서 Resolution inference rule은 sound 하지만 complete 하지는 않다. 그러나 Proof-by-Contradiction을 이용하면 sound하고 complete한 Theorem Prover를 만들 수 있다. 즉 KB |= A를 증명하기 위해 먼저 formula A를 부정하여 KB에 추가하고, 이 확장된 지식 베이스가 inconsistent하다.

즉 contradiction이 생긴다는 것을 증명하는 망법으로 Sound & Complete한 Theorem Prover를 만들 수 있다는 것이다.

 

 Example 9.

 

 

* Transfer to Conjunctive Normal Form
 - Eliminate ⇔, replacing a⇔b with (a⇒b)∧(b⇒a)

 - Eliminate ⇒, replacing a⇒b with ¬a∨b
 - CNF requires ¬ to appear only in literals, so we "move ¬ inwards" by repeated application of the following equivalences:
   · ¬¬a≡a (double-negation elimination)
   · ¬(a ∧ b) ≡ (¬a ∨ ¬b) (De Morgan)
   · ¬(a ∨ b)  ≡ (¬a ∧ ¬b) (De Morgan)
 - Apply the distributive law, distributing ∨ over ∧ wherever possible

 

 Example 10.

* Horn clauses
 - A clause in conjunctive normal form contains positive and negative literals and can be represented in the form

  > non-definite한 clause를 제한하는 clause. (positive literal이 많아봐야 1개, or 0개)

 

Horn Clause 는 Clause 인데 positive literal 를 많아야 1 개 포함하는 즉 , positive literal 을 1 개 포함 하든지 혹은 포함하지 않는 Clause 를 말한다 .

이는 다음과 같은 형태의 지식을 의미한다.
① A 1 ∧ A 2 ∧ … ∧ A n ⇒ B where A 1 , … A n and B are atomic formula.
이러한 지식은 rule 형태 왼쪽 part(antecedent) 와 오른쪽 part (consequent)로 나누어진다 .

그런데 오른쪽 part 한 개의positive formula B를 head 라 부른다 .

여기서 A 1 ∧ A 2 ∧ … ∧ A n ⇒ B ≡¬A 1 ∨ ¬A 2 … ∨ ¬A n ∨ B 이므로 Horn Clause이다 .

만약 B 대신 f(거짓) 이어도 positive literal 이 하나도 없는 Horn Clause 이다.
② 단순히 B 형태 즉 한 개의 positive literal 로 fact 라고 부른다 .
이렇게 지식을 Horn Clause 로 표현하면 규칙 (rule) 과 사실 (fact) 로 볼 수 있겠다.

 

 Example 11.

 

* SLD resolution (for Horn clauses)
일반적인 Resolution rule에서 resolution 시킬 두 개의 Clause를 찾는 문제, serching problem이 발생하는데 SLD Resolution은 항상 바로 앞에서 Resolution하여 발생한 Clause (Resolvent)를 다음 Resolution 할 Clause으로 늘 사용하므로 나머지 한 개의 Clause 만을 찾으면 되므로 효율적인 진행이 가능하다.

 

또한 Horn Clause의 형태는 Theorem Proving 할 때 rule 형태의 오른쪽 part인 head, 예를 들어 B를 목적(Goal)으로 하여 왼쪽 part인 antecedent part, conjuction, 예를 들어 A1∧A2∧...∧An을 각 fact들을 부목적(Subgoal)으로 하여 반복적으로 (recursive 하게) 각 목적을 달성하는 방법(Backward 방식)을 사용할 수 있다.

 

 Example 12.

* Forward and Backward Chaning
 - forward chaining: starts with facts and finally derives the query
 - backward chaing: starts with the query and works backwards until the facts are reached

 => There are treadeoffs between forward and backward chaing methods. 

Some inference engines employ both methods.

  For example, in forward chaining: tradeoffs: time vs space
  · Assert(A⇒B); KB = {A⇒B}
  · Assert(A);      KB = {A⇒B, A, B}; by forward chaing
  For example, in backward chaing:
  · Assert(A⇒B); KB = {A⇒B}
  · Assert(A);     KB = {A⇒B, A}
  · Ask(B);         KB = {A⇒B, A, B} The answer is yes by backward chaining

 

* Computability and Complexity
 - The truth table method determines every model of any formula in finite time.
 - The sets of unstatisfiable, satisfiable, and valid formulas are decidable.
 - T(n) = O(2의 n제곱)
 - Optimization: semantic tree, grow exponentially in the worst case.
 - At resolution, the number of derived clauses grows exponentially with the number of clauses in the worst case.
 - S. Cook: the 3-SAT problem is NP-complete(P: polynimial)
 - 3-SAT is the set of all CNF formulas whose clauses have exactly three literals.
 - For Horn clauses: the computation time for testing satisfiability grows only linearly as the number of literals in the formula increases.

 

 

 아주대학교 정보통신대학원 김민구 교수님의 인공지능 강의를 바탕으로 작성하였습니다.

 학습 목적으로 포스팅 합니다.