2019년 9월 30일 월요일

Polybase를 활용한 ETL(mssql -> hadoop) 라이브러리 개발

Polybase를 활용한 ETL(mssql -> hadoop) 라이브러리 개발

ssis, sqoop 등 etl 툴이 많지만 db to db가 아닌 mssql에서 hadoop으로 데이터를 내린다면 polybase를 활용하여 쉽게 해결할 수 있다.

구조(준비물)은 다음과 같다.

1. EtlSqlOperator.java
- Connect mssql, Read sql query file, Run sql, Delete/Move hdfs path
2. EtlSqlOperator.sh
- Run shell script
3. DelHdfsPath.sh
- Delete path if exists
4. MoveHdfsPath.sh
- Move path if exists
5. sql query file
- CETAS query
6. sqljdbc.jar
- For db connection


사용방법
원하는 경로에 etl 디렉토리(상위)를 만들었고 etl 디렉토리 하위에는 sql, lib 디렉토리가 있다. lib에는 jdbc driver를 넣어놨고 sql 디렉토리에는 실제로 날릴 CETAS 쿼리들이 들어있다. 나머지 쉘 스크립트나 java 파일은 etl 디렉토리에 넣어놨다.

1. EtlSqlOperator.java를 자신의 상황에 맞게 수정해서 컴파일 한다.
2. 쿼리 구문을 작성해서 sql 디렉토리 하위에 넣는다.
3. EtlSqlOperator.sh에 2번에서 작성한 sql 쿼리 파일을 추가해서 실행한다.



소스, 드라이버 등 파일은 깃헙에 올려놓았다.
깃헙 주소 : https://github.com/parksuseong/ETL_Library



파일 설명 부분

EtlSqlOperator.java 

import java.sql.Connection;
import java.io.File;
import java.io.FileReader;
import java.io.FileNotFoundException;
import java.io.IOException;

import java.sql.DriverManager;
import java.sql.SQLException;
import java.sql.Statement;
import java.sql.ResultSet;
import java.text.SimpleDateFormat;
import java.util.Date;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;

public class EtlSqlOperator {

public static void DelPath(String str){

try {
Runtime runtime = Runtime.getRuntime();
Process process = runtime.exec("path/etl/DelHdfsPath.sh " + str );

InputStream is = process.getInputStream();
InputStreamReader isr = new InputStreamReader(is);

BufferedReader br = new BufferedReader(isr);

String line;
   // this is trick
while((line = br.readLine()) != null) {

System.out.println(line);
}


} catch (IOException e1) {
System.out.println("del error..........");
// TODO Auto-generated catch block
e1.printStackTrace();
}

}


public static void MovePath(String str1, String str2){

try {
Runtime runtime = Runtime.getRuntime();
System.out.println("------------------------------------------------------------");
System.out.println("from " + str2 + " to " + str1);
System.out.println("------------------------------------------------------------");
String tmptmp = "path/etl/MoveHdfsPath.sh " + str1 + " " + str2+"*";
Process process = runtime.exec(tmptmp);

InputStream is = process.getInputStream();
InputStreamReader isr = new InputStreamReader(is);

BufferedReader br = new BufferedReader(isr);

String line;
   // this is trick
while((line = br.readLine()) != null) {

System.out.println(line);

}


} catch (IOException e1) {
System.out.println("move error.........");
// TODO Auto-generated catch block
e1.printStackTrace();
}

}


public static void main (String args []) {

String sql = "";
System.out.println("ETL Start...");
System.out.println("PARAMETER FILE NAME IS " + args[0]);

// sql file read
System.out.println("------------------------ READ SQL FILE ----------------------");
try{
File file = new File(args[0]);
FileReader filereader = new FileReader("path/etl/sql/"+file);
int singleCh = 0;
while((singleCh = filereader.read()) != -1){
sql += (char)singleCh;
}
filereader.close();
}catch (FileNotFoundException e) {
// TODO: handle exception
System.out.println(e);
}catch(IOException e){
System.out.println(e);
}


Connection conn = null;
Statement stmt = null;
ResultSet rs = null;

try {

// connect db
Class.forName("com.microsoft.sqlserver.jdbc.SQLServerDriver");
conn = DriverManager.getConnection("jdbc:sqlserver://xx.xxx.x.xx:1433","userid","password");
stmt = conn.createStatement();



int start_idx = sql.indexOf("LOCATION='/")+10;
int end_idx = sql.indexOf(",",10);
// create destination path
String path_str = sql.substring(start_idx,end_idx-1);
// create temp path
String tmp_path = "/user/BIGDATA/DW/STG"+path_str;
// delete temp path if exists
System.out.println("------------------------------ destination path ------------------------------ \n" + path_str);
System.out.println("------------------------------ tmp path ------------------------------ \n" + tmp_path);
System.out.println("--------------------------------------------------");
DelPath(tmp_path);
// create tmp_sql
String tmp_sql = sql.replace(path_str, tmp_path);
System.out.println("------------------------------ tmp sql ------------------------------\n" + tmp_sql);
// run tmp_sql
System.out.println("------------------------------ tmp_sql run ------------------------------");
int result = stmt.executeUpdate(tmp_sql);
// delete destination path if exists
System.out.println("------------------------------ del func ------------------------------");
DelPath(path_str);
System.out.println("------------------------------ del complete ------------------------------");
//move to destination from temp path
MovePath(path_str,tmp_path);
System.out.println("------------------------------ move succ ------------------------------");
} catch (SQLException e) {
e.printStackTrace();
} catch (ClassNotFoundException e) {
e.printStackTrace();
} finally{
try {
if (rs!=null) rs.close();
if (stmt!=null) stmt.close();
if (conn!=null) conn.close();
} catch (SQLException e) {}
}


}

}


EtlSqlOperator.sh



DelHdfsPath.sh


MoveHdfsPath.sh



SQL_TEST_TABLE (example)




주의할 점은 지우고 쓰는 것을 sync를 맞춰야되서 나름대로의 trick을 넣어뒀다.
// this is trick
그렇지 않으면 쓰는동안 지워버리는 문제가 생길 수 있기 때문이다. 그때의 에러는 해당 경로가 존재하지 않는다고 나올 것이다.

2019년 9월 28일 토요일

Artificial Intelligence - 서술 논리(Predicate logic)에 대하여

서술 논리라 함은 1차 서술 논리(first-order Predicate Logic)라고도 하는데 아주 강력한 심볼릭 언어이다. 명제논리보다 훨씬 더 표현력이 강해서 복잡할 수 있지만 전반적인 흐름은 비슷하다.

가령 명제논리에서 로봇-7이 로봇-12보다 오른쪽에 있다는 객체들의 관계를 표현하기에 어렵다. (로봇과 좌표가 많은 경우 따져야하는 경우의 수가 너무 많아지기 때문이다.)
ex) 로봇 7이 (x,y)좌표 (35,79)에 존재한다. 로봇 12가 (x,y)좌표 (10,93)에 있다....


서술 논리(First-order Predicate Logic)의 정의


서술 논리의 문법을 정의하기 위하여 먼저 Term을 정의한다. Term은 세상이 객체(Object)들로 구성되었다고 가정하면 이 객체를 가리키는 혹은 표현하는 언어의 일부이다. 이를 이용하여 추후에 문장(Formula)를 구성하게 된다.

Term은 3가지의 방법으로 사용된다.

첫째는 constant term으로, 예를 들어 John, Mary 등과 같이 세상의 객체인 John이라는 남자, Mary이라는 여자를 가리키는 의미로 사용할 수 있다. John과 Mary 앞의 정의 K 라는 집합에 원소가 될 수 있다.

두번째 방법으로 변수(variable) term으로, 예를 들어 x, y, z 등을 변수 심볼이라 하면, 이 변수들은 앞의 정의에서 사용한 집합 V의 원소들이 된다. 변수 term 들도 세상의 객체를 가리켜야 한다. 예를 들어 변수 x를 John이라는 남자를 가리키게 할 수도 있고 Mary라는 여자를 가리키는 변수로 사용할 수도 있다.

세번째로 함수(function) term이 있다. 물론 함수 term도 세상의 객체를 가리켜야 한다. 예를 들어 John의 아버지를 표현할 때 함수 term, father-of(John)로 표현할 수 있겠다. 물론 father-of(John)도 john의 아버지 객체를 가리킨다. 이때 father-of는 function symbol로 argument 1개를 갖는 함수 심볼로 앞의 정의 F 집합의 한 원소가 되며, 함수 f(x)의 뜻은 x의 아버지를 나타낸다. 이러한 함수를 1-place function이라고 한다. 

함수의 argument도 반드시 term이어야만 한다. Term은 상수, 변수, 함수 term이 되므로 재귀적(recursive)으로도 사용할 수 있다. 예를 들어 John의 아버지의 아버지는 father-of(father-of(John))으로 표현할 수 있으며 이 함수 term은 John의 할아버지인 객체를 나타낸다.

서술논리의 집합 P는 다음과 같이 정의된다.


서술 논리의 문장(Formula)는 객체와 객체의 관계를 표현하는데 사용되며, 이러한 관계를 나타내는 심볼을 Predicate symbol이라고 한다. 예를 들어 John이 Mary를 사랑(loves)한다면 loves(John, Mary)로 표현 할 수 있는데 John과 Mary는 상수 term이고, loves는 2개의 argument(term)를 갖는 2-place predicate symbol이다. 이 때 loves는 앞에서 정의 한 집합 P 의 원소가 된다.

또한 function term과 혼동하지 말아야 할 것은 predicate는 서술 논리의 문장인 formula를 만들며 John과 Mary의 관계, 즉 John이 Mary를 사랑하는 관계를 나타내며, 이 문장은 참일 수도 거짓일 수도 있다. 반편 함수 term, 예를 들어 father-of(John)은 객체를 나타내어 predicate의 argument 혹은 function의 argument로 사용되므로 관계를 나타내는데 사용될 수 없다. 만약 어떤 사람이 Smith가 John의 아버지라는 관계를 말하고 싶다면 관계를 나타내는 predicate, 예를 들어 2-place predicate symbol is-a-father-of를 사용하여 is-a-father-of(Smith, John) 표현할 수 있다.


그렇다면 서술 논리로 명제를 표현해보자.
명제 : 똘똘이는 개이다. 개는 달릴 수 있다.

똘똘이는 개이다.
constant symbol : 똘똘이
1-place predicate symbol : Dog(x) ; x is dog
Formula : Dog(똘똘이)

개는 달릴 수 있다.
1-place predicate symbol : Runable(x) ; x can run
Formula : ∀x Dog(x) ⇒ Runable(x)

명제에서 개를 constant라고 한다면 세상에는 개가 한마리 밖에 존재하지 않으므로 개는 1-place predicate symbol로 정의하여 Dog(x), 즉 개들의 집합으로 본다. 반면에 똘똘이(term)는 하나의 객체를 의미한다.
만약에 개를 constant로 사용하여 Runable(개)라고 표현하면 세상에 개는 한마리만 있는 세상에서나 가능한 이야기다.

즉 ∀x Dog(x) ⇒ Runable(x)로 정의할 수 있다.(모든 x에 대해서 x가 개라면 달릴 수 있다.)

그렇다면 ∀x Dog(x) ∧ Runable(x)는 왜 안될까?
모든 x에 대해서 x는 개이고 개는 달릴 수 있다. 이 말은 세상에 개만 존재하는 세상이라면 어울릴 수 있겠지만 그게 아니기 때문에 ∧(conjunction)로 표현하면 어색한 표현이 될 수 있다.
정리하면 ∀x Dog(x) ⇒ Runable(x)는 개는 달릴 수 있다는 의미에 가깝지만 ∀x Dog(x) ∧ Runable(x)는 세상에 모든 것은 개이고 개는 달릴 수 있다 라는 의미에 가깝다.

다음은 다양한 예이다.



이외에도 앞서 포스팅했던 명제논리 편에서 설명했던 Formula에 적용되는 용어인 valid, satisfiable, unsatisfiable, model, entailment 등 또한 모두 똑같이 통용된다.



한가지 예를 들어서 상기시켜보자.
John loves Mary
John's brother loves Mary's sister.

온톨로지를 정의하면
Constant symbols : John, Mary
1-place function symbol: brother-of(x) ; brother of x / sister-of(x) ; syster of x
2-place predicate symbol: love(x,y) ; x loves y.

love(John,Mary)
love(brother-of(John),sister-of(Mary))

객체로는 John, Mary, John's brother, Mary's sister 등이 존재할 것이고 매핑함수 현실세계 W와 논리세계를 매핑해주는 함수 I는 저 객체들을 가리킬 것이다.

한번 더 해보자
다음은 소크라테스 문제이다.
KB = {∀x man(x) ⇒ mortal(x), man(Socrates)}
KB |= mortal(Socrates) ? 답은 yes.

man(Socrates) ⇒ mortal(Socrates)
≡ ┐man(Socrates) ∨ mortal(Socrates)
따라서 ┐man(Socrates) 가 false이기 때문에 mortal(Socrates) is true가 된다.

위에서 설명된 내용은 모두 집합이라고 보고 이를 집합에 의한 의미론이다 하여 Set theoretic Semantics 혹은 객체를 가리킨다 하여 Denotation Semantics 이라고 불리기도 한다.




가족 관계 트리를 보자.


사람들의 이름이 상수 term이 되고 2개의 predicate symbol을 정의했다.
1-place predicate female(x): x is a female
3-place predicate child(x, y, z): x is a child of y and z

Karen은 여자이고 Oscar A는 karen과 franz의 자식이다 라는 표현을 서술 논리 formula로 female(karen), child(oscar A. karen, franz) 로 정의했다. 소문자 karen은 서술 논리에서 사용하는 상수 symbol이고 대문자 Karen은 World에 존재하는 객체 Karen을 나타내기 위해 구분하였다.

Kind는 child를 말한다. (책이 독일어가 가끔씩 나온다.)

child(eve, anne, oscar)는 그림에서 보듯 참이다. 그럼 child(eve, oscar, anne)가 참이 되려면 무슨 지식이 더 필요할까? 위에 가족관계 트리 아래쪽에 Relation에 없는 것을 보니 바로 True로 하면 안될 것 같다.


명제 논리에서 설명한 A ⇔ B : A if and only if B (equivalence) A가 참이면 B도 참, B가 참이면 A도 참 이라는 지식이 더 필요하다.

그리고 descendant라는 함수를 통해 x는 y의 후손이다 라는 것을 정의할 수 있다.
x는 y, z는 아이인데 그런 z가 존재하거나 또는 x가 u, v의 자식이고 u는 y의 후손이다라고 reculsive하게 정의할 수 있다.

마침내 아래처럼 Knowledge Base를 정이하여 child(eve, oscar, anne)도 참이라는 결론을 Derivation 할 수 있다.



서술 논리에서도 명제 논리처럼 entail하는지 계산할 수 있는 derivation 프로그램인 theorem prover가 필요하다. 이를 위하여 궁극적으로 resolution-refutation 방법을 사용하기 위하여는 먼저 CNF(Conjunctive Normal Form)으로 변환하여야한다. 이를 위해 서술 논리에서는 명제 논리에 없는 한정사를 제거하는 과정이 필요하다. 먼저 prenex normal form으로  만들고, existential quantifier를 skolemization을 이용하여 제거하고 최종적으로 universal quantifier 제거하게 된다. 또한 unification process도 필요하다.



반면에 서술 논리에서 term을 사용하여 객체를 나타내게 되는데 우리 종종 같은 객체를 다른 이름으로 사용하는 경우가 많다. 예를 들어 John's father를 function term으로 father-of(john)이라고 표현할 수도 있지만, John's father가 Smith라고 한다면, 우리는 쉽게 father-of(john) = smith라는 관계를 표현 할 수 있다.  이 때 = symbol을 어떻게 처리할 것인가 하는 문제가 생긴다. 한 가지 방법은 = symbol을 predicate symbol로 간주하는 경우이다 (물론 이 때 문법은 일반 predicate와 다르게 양쪽에 term이 오는 형식으로 2-place predicate symbol이다).
이럴 경우 = symbol은 다음 처럼 axiom이 필요하게 된다.


다른 한가지 방법은 = symbol을 특수 연산자로 정의하여 사용할 수 있지만 이는 구현(control)의 방법으로 해결하는 것으로 순수한 논리 언어라고 볼 수 없다. 어쨌든 논리 equality 심볼은 많은 문제점을 내포하고 있어서 지식 표현 시스템에서도 equality 사용을 허용하지 않는 경우도 존재한다고 한다.

equality axioms를 적용하여 표현해보자.
( = symbol에 이렇게 복잡한(?) 의미가 있다니...)

John’s father loves Mary.
John’s father is Smith.
Ontology:
Constant symbols: John , Mary , Smith
2-place predicate symbol: loves(x, y)  ; x loves y.
1-place function symbol: father-of(x)  ; x’s a fther.
KB , a set of formulas:
loves(father - of(John), Mary)
father - of(John) = Smith
KB╞ loves(Smith, Mary) 
by the equality axioms



prenex normal form은 quantifier를 모두 앞으로 빼는 것이다.


예를 들어보자.


Ontology:
Constant symbol: 0, b, N
Function symbols:  abs(x) ; x
a(n) ; 𝑎𝑛
minus(x, y)  ; x- y
Predicate symbols: el(x, y)  ; x ∈ y , gr(x, y)  ; x > y



결국 아래처럼 Quantifier를 앞으로 보낸다.


이걸 step을 따라가보면 다음과 같다.
보기엔 어렵지만 한번 이해를 해두기 위해 손으로 적으면서 step을 따라가야 한다.


언어는 훈련이 되어야 사용이 가능한 것이다.

모든 Predicate logic formula는 prenex normal form으로 바꿀 수 있다.
분명한 것은 쉽지 않다.
온톨로지를 정의하는 것 조차 상당한 훈련이 필요하다.


이후 Skolemization를 하고 똑같이 Resolution을 하는 것은 명제 논리와 같다.
(Skolemization은 existential quntifier를 제거하는 것을 뜻한다.)


지금까지 서술논리에 대해서 어느 정도 설명했는데 서술논리는 변수와 universal quantifier가 사용되기 때문에 명제 논리보다 표현력이 뛰어나다고 볼 수 있다.

Deduction theroem은 다음과 같다.
지금까지 계속 이야기했던 내용과 비슷하다. 결국 어떤 formula가 true인지를 증명하려면 부정을 해서 KB에 넣어서 이게 모순이 되는지를 확인하는 것이다.

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


다음을 보자.



모두가 그(Henry)의 어머니를 안다. Henry는 어떤 사람을 아는가?
Q를 Henry가 y를 안다를 부정하자.
그리고 KB에 넣으면 이는 모순이 되기 때문에 Henry는 어떤 사람을 알게 된다.

다음은 다른 이야기이다.
Resolution Rule은 sound하다. 하지만 complete하지 않다.

유명한 러셀(Russell)의 역설(paradox)이다.


어떤 마을에 이발사가 존재한다. 그 사람은 스스로 면도를 하지 못하는 모든 사람들의 면도를 해준다.
이 문제는 아무리 Resolution을 해도 contradiction을 만들 수가 없다. 즉 sound는 해도 complte하지않는다.

따라서 Factorization이 필요하다.


위키를 참조하면 다음과 같다. (일명 이발사의 역설이다.)
마을에서 단 한 명의 이발사(남성)는 스스로 수염을 깎지 않는 모든 사람의 수염을 면도하고 그 이외의 사람의 수염은 깎지 않는다고 가정한다.
여기서 문제는 "이발사는 자신의 수염을 면도하는가?"이다.

이 질문에 답변할 경우 모순이 발생한다. 이발사는 스스로 면도를 하지 않는 사람에게만 면도를 수행하므로 스스로 면도를 할 수 없다. 이처럼 스스로 면도를 한다면 그는 이발사 일을 그만두게 된다. 이와 반대로, 이발사가 스스로 면도를 하지 않는다면 그는 이발사에게 면도를 받는 사람의 그룹에 속하게 되므로 이발사로서 그는 스스로 면도를 해야 한다.


이번에는 CNF로 바꾸는 예를 들어보자.

Everyone who loves all animals is loved by someone.
모든 동물을 좋아하는 사람이 있다면 그 사람을 좋아하는 사람이 있다.

CNF for first-order logic: similar to the propositional case.
Ex) ∀x [∀y Animal(y )⇒ Loves(x,y)]⇒[∃y Loves(y,x)]


1. Eliminate implications: (임플리케이션을 지운다.)
∀x ┐ [∀y ┐Animal(y)∨Loves(x,y)]∨[∃y Loves(y,x)]

2. Move ┐ inwards:
┐∀x P becomes ∃x ┐P (좌측이 우측으로 바뀜.)
┐∃x P becomes ∀x ┐P (좌측이 우측으로 바뀜.)
∀x [∃y ┐(┐Animal(y) ∨ Loves(x,y))] ∨ [∃y Loves(y,x)]
∀x [∃y ┐┐Animal(y) ∧ ┐Loves(x,y)] ∨ [∃y Loves(y,x)]
∀x [∃y Animal(y) ∧┐Loves(x,y)] ∨ [∃y Loves(y,x)]

3. Standardize(Rename) variables: (변수 이름을 바꿀 필요가 있으면 바꿔준다.)
∀x [∃y Animal(y) ∧  ┐Loves(x,y)] ∨ [∃z Loves(z,x)]

4. Skolemize: (Skolemize을 한다.)
∀x [Animal(F(x)) ∧  ┐Loves(x,F(x))] ∨ Loves(G(x),x)

5. Drop universal quantifiers: (universal quantifiers을 지운다.)
[Animal(F(x)) ∧  ┐Loves(x,F(x))] ∨ Loves(G(x),x)

6. Distribute ∨ over ∧: (분배법칙 적용)
[Animal(F(x)) ∨ Loves(G(x),x) ]
∧[ ┐Loves(x,F(x))∨Loves(G(x),x)]

그렇다면 다음을 보자.
Everyone who loves all animals is loved by someone.
Anyone who kills an animal is loved by no one.
Jack loves all animals.
Either Jack or Curiosity killed the cat, who is named Tuna.
Did Curiosity kill the cat?


온톨로지
Constants: Jack, Tuna, Curiosity
1-place Predicates: Animal(x) ; x is an animal.
Cat(x) ; x is a cat.
2-place Predicates: Loves(x,y) ; x loves y.
Kills(x,y) ; x kills y.

Example for resolution
1. ∀x [∀y Animal(y) ⇒ Loves(x,y)] ⇒ [∃y Loves(y,x)]

2. ∀x [∃y Animal(y) ∧ Kills(x,y)] ⇒ [∀z ┐Loves(z,x)]

3. ∀x Animal(x) ⇒ Loves(Jack,x)

4. Kills(Jack,Tuna) ∨ Kills(Curiosity,Tuna)
잭이 튜나를 죽였거나 Curiosity가 튜나를 죽였거나 둘 중에 하나다.

5. Cat(Tuna)

6. ∀x Cat(x) ⇒ Animal(x) ; Additional knowledge

┐G. ┐Kills(Curiosity,Tuna) : Refute the query
Curiosity가 튜나를 죽였나?

Transform to CNF
1. Animal(F(x)) ∨ Loves(G(x),x)

2. ┐Loves(x, F(x)) ∨ Loves(G(x),x)

3. ┐Animal(y) ∨ ┐Kills(x1,y) ∨ ┐Loves(z,x1)

4. ┐Animal(x2) ∨ Loves(Jack,x2)

5. Kills(Jack, Tuna) ∨ Kills(Curiosity, Tuna)

6. Cat(Tuna)

7. ┐Cat(x3) ∨ Animal(x3)

┐G. ┐Kills(Curiosity, Tuna)

결론 : Curiosity가 튜나를 죽였다.


포스팅 내용이 뒤죽박죽이고 설명을 잘 못했는데 부족한 점은 나중에 기회가 되면 다시 보완해야겠다. (사실 쓰면서도 한번에 집중하지 않으면 헷갈리고 내용이 어렵다.)



- 참고
아주대학교 정보통신대학원 인공지능(Artificial Intelligence(김민구 교수님))의 강의를 수강하며 배운 내용을 바탕으로 정리하였습니다. 그리고 강의 내용은 ertel's slide가 참고 되었습니다. 학습 목적으로 포스팅 합니다.


2019년 9월 23일 월요일

Artificial Intelligence - 명제 논리(Propositional logic)에 대하여

논리(Logic)은 심볼릭 표현 언어이다. 인간이 표현하는 언어를 자연어라고 부르는데 대부분 심볼릭한 언어라고 볼 수 있다. 하지만 자연어에서는 의미가 불분명한 경우가 많은데 그 것들은 수학적으로 정의하기가 어려울 것이다.


논리 언어에는 여러 종류가 있지만 가장 기본적인 언어는 명제 논리(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를 생성하는 규칙이다.


위처럼 Modus ponens rule에는 counter example이 존재한다.

이때문에 조금 더 일반화(?) 된 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 만 될 수 있다.)


한가지 예를 들어서 참인지 거짓인지 밝혀보자.

과연 three girls가 모두 참일 수 있을까?




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가 참고 되었습니다. 학습 목적으로 포스팅 합니다.