composite 실습


상수(소문자) : f(a) / 변수(대문자)


s1 = {g(X,Y)/Z}    S2 = {a/X, b/Y, c/W, d/Z}


1) composition s1s2

s1s2 = { g(a,b)/Z, a/X, b/Y, c/W}


2) composition s2s1

s2s1 = {a/X, b/Y, c/W, d/Z}



#Step 1. 합성 순서대로 합집합 연산


#Step 2. 상수 쪽이 변수인 것을 상수화 함.


#Step 3. 중복 되는 것(X/X, 또는 a/X와 b/X)을 우선순위에 따라 제거. 보통 왼쪽이 우선순위가 높음

'Courses > `2012 AI' 카테고리의 다른 글

composite 실습  (0) 2012.05.07
Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01

a) Anyone meeting Tom is falling in love with him.


b) Anyone who loves Tom is happy.


c) Jane did not meet Tom and Kate met Tom


atomic : meet(X, Y), love(X, Y), happy(Z)



1) to predicate form

a) ∀x meet(x, Tom) -> love(x, Tom)

b) ∀x love(x, Tom) -> happy(x)

c) ¬meet(Jane, Tom)∧meet(Kate, Tom)


2) to clause form

P->Q : ¬P∨Q 의 형태로 없앰 (implacte 를 OR로 변환)

? 근데 한정자가 들어가는지 안들어가는지는 모르겠음.. 확인해봐야 할듯

¬∀∧∨∃


a) ¬meet(x, Tom)∨love(x,Tom)


b) ¬love(x,Tom)∨happy(x)


c) ¬meet(Jane, Tom)  // AND 는 그냥 아래줄에 씀

    meet(Kate, Tom)

'Courses > `2012 AI' 카테고리의 다른 글

composite 실습  (0) 2012.05.07
Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01

5. LISP

 

  리습은 인공지능을 할때 쓰이는 프로그래밍 언어 중 하나이다. 최초로 1958년 MIT의 존 매카시가 개발하였다. 리스프는(LISP)란 이름은 List Processing (리스트 처리) 의 줄임말 이다. 리스프는 여타의 다른 언어들과는 상당히 다르다. 람다 계산법(Lambda Calculus)에 바탕을 두고, 기호 데이터(Symbolic data)를 다루는 문제 풀이에 알맞은 언어로 설계되어 있어 있어, 아톰(Atom)이나 리스트(list) 같은 전혀 새로운 데이터를 쓰고 있다. 리스프는 최초의 개발자 존 매카시가 모든 것을 한꺼번에 개발 한 언어가 아니다. 초창기의 리스프는 산술 계산같은 것이 느린 단점을 지니고 있었고, 사용하기가 조금더 복잡하였다. 하지만, 세월이 지나면서 자신들이 필요한 부분을 보완하고 추가 해가며 발전해 와, 이제는 인공지능에서는 매우 중요한 언어로 자리잡고 있다. 이때문에, 리스프는 대단히 많은 변종들이 존재하며 (ZetaLisp, Franz Lisp, InterLisp 등) , 일반적으로 리스프 라고 하면, 이러한 변종들을 통칭하여 가리킨다.

 

 - Symbolic Expression

 

  위에서도 언급했듯이, Lisp은 전혀 새로운 데이터 타입을 사용한다. Atom 과 List 가 바로 그것이다. 그리고, 이러한 2개를 가리켜 Symbolic Expression 이라고 한다. 그렇다면 이들이 무엇인지 한번 알아보자.

 

1) Atom : Letters(문자 - 영문으로 대소문자 모두)

             Numbers (숫자)

             Characters (*, &, %, ...)

  

2) List : 공백에 의해 구분되는 Atom 또는 다른 리스트들이 괄호 안에 들어가 있는것

            (  (1 2 3 4) , (1 (2 3) 4 ),  ......)

 

  이렇게 2개의 자료형을 사용자가 입려가면, 리스프의 인터프리터(Inerpreter) 는 해당 결과를 화면에 출력한다. Atom을 입력하면, 있는 그대로를 출력하고, List를 입력하면 가장 처음에 나와있는 function definition 을 참조하여, 그에 알맞는 결과를 출력한다.

 

입력 : ( * 10 9 )                         출력 : 90

입력 :  (- (* 10 9 ) ( * 8 10))        출력 : 10

입력 : (list a b c d e)                 출력 : (a b c d e)

입력 : (nth 2 '(a b c))                 출력 : c               (어퍼스트로피 빼먹지 않게 주의)

 

위의 마지막 예제에서 '(a b c) 처럼, 어퍼스트로피가 쓰였다. 이는 (quote (a b c)) 랑 같은 것으로, 괄호 안을 함수로 취급하지 말고 있는 그대로 사용하라(또는 출력하라) 라는 뜻이다. 아래의 예제를 보면 이해가 쉽게 될 것이다.

 

입력 : (quote (+ 1 6))                  출력 : (+ 1 6)

입력 : ( '(a b) )                          출력 : (a b)

 

 

 - Function Definition

 

 리스프도 다른 여타의 언어와 마찬가지로 함수를 정의 하고, 사용 할 수 있다. 함수의 정의법은 아래와 같다.

 

(함수이름 / 함수 변수 목록/ 함수 내에서 수행할 계산)

 

예를드련, 인자 x를 받아서, x의 제곱을 리턴하는 함수는

 

(defun double(x) (* x x)) : x를 인자로, 받고 x를 제곱해서 리턴한다.

 

 

- Condition

 

 조건문으로, 형태는 (cond ( (조건1) (Action)) ( (조건2)(Action)) ( (조건3....

 이런식으로 나간다.

 

 (cond ((< x 0 )(-x)) (t x))  : 만약 x가 0보다 작으면 - x를 출력하고, 0보다 크거나 같으면 그냥 x를 리턴하라.

 (defun (absoulute-value (x) (if(< x 0) ( -x) x)) : absolute-value 라는  함수를 선언한다. 만약 0보다 작으면 - x로 리턴

                                                                     그렇지않으면 그냥 x를 리턴하라. 

 

 

- Binding Variables

 

   (setq <symbol> <form>) : symbol 은 form의 값을 갖게 한다. (단, symbol은 계산 되지 않는다. 어퍼스트로피가 붙은 상황)

   (set <place> <form>) : symbolic expression  <place>를 <form>으로 바꾼다. (<place>는 계산된다.)

   (setf <place> <form>) : <place>가 <symbol>이면 setq와 같이 동작하고, 그렇지 않으면 set과 같이 동작 한다.

 

(setq x 1) = 1

(set a 2 ) = ERROR  (a cannot be evaluated)

(set 'a 2) = 2

(+ x a ) = 3

(setq 1 '(a b)) = (a b)

(set (car 1) p) = p

1 = (p b)                          //(car 1) = a이고, a는 p로 치환되었으므로,  1 = (p, b) 이다.

 

위의 예제를 그대로 setf로 바꾸면 아래와 같다.

 

(setf x 1) = 1

(setf a 2) = 2

(+ a x) = 3

(setf 1 '(a b)) = (a b)

(setf (car1) p) = p

1 = (p b)

 

 

let( (<Symbol> <function>)  (<Symbol2><function2>)(<symbol3 .....)

 

   let은 괄호 안에에서 여러개의 변수를 다른 값에 할당할때에 사용한다.

 

 

- Else

 

  car - return the first element.

  cdr - return the rest element

  cons - constructing a list by its parameter (받은 파라미터들로, 리스트를 새로 만든다.)

  append - attach each parameter to make lise (받은 파라미터들을 연결하여 리스트를 만든다.)

 

  (car  '(a b c d)) : a

  (cdr  '(a b c d)) : b c d

  (first '(a b c d)) : a

  (second '(a b c d)) : b

  (cons 'a '(b c)) : (a b c)

  (cons '(a b) '(c d)) : ( (a b) c d)

  (append '(a b) '(c d)) : (a b c d)

 

 

- Recursion

 

 리습은 함수형 언어 이기때문에, 특정 문제를 풀기 위해서는 recursion을 통해 계속해서 함수를 호출 해 줘야 한다. 하지만, 실제로 해보면 알 수 있듯이 recursion을 만드는 것이 그리 쉬운 것 만은 아니다. 그래서, 재귀의 형태를 만들기 쉽도록 하는 몇가지 방법에 대해서 알아 보자.

 

1) Double-Test Tail Recursion

 

기본 형태는  (Defunc func(x) (cond (endtest_1 endvalue_1)(endtest_2 endvalue_2)(T (func reduced-x))))

 

예제를 보자. 다음의 예제는 인풋으로 들어온 list 또는 atom이 짝수를 포함하고 있는지를 보는 함수 이다.

 

defun anyEvenP(x) ( cond ((null x) nil)((even (car x) T)((t (anyEvenP(cdr x)))))

 

만약, 리스트가 비었으면, nil을 리턴, 그렇지 않고, 리스트의 가장 처음 x가 짝수이면, T(true)를 리턴, 그것도 아니라면 리스트의 맨처음 을 제외한 나머지 부분을 다시 anyEvenP 함수를 재귀적으로 호출한다.

 

 

2) Single-Test Tail Recursion

 

  위에서 했던, Doble-Test Tail 이 2개의 조건으로 체크를 했다면, 이것은 한개로 체크를 하는 것이다. 따로 예제는 들지 않겠다.

 

3) Single-Test Augmenting Recursion (한개의 테스트로 값을 늘려가는)

 

  조건은 한개지만, 리커션이 호출될 때 마다, 특정값이 증가 하도록 만드는 리커션이다. 흔히 1+2+3+4+ ... 를 리커션으로 구할때 각 +와 + 사이의 값이 1씩 증가 하나. 이처럼 리커션이 호출될 때마다 해당 항의 값이 증가하는 재귀함수를 가리킨다.

 

4) Conditional Augmentaton (조건부 값 상승)

 

  조건에 따라서, 리커션의 각 항을 값을 늘리거나 늘리지 않을때 사용하는 리커션이다. 함수 howManyNum 이라는 것이 있을때, 리스트에서 숫자의 갯수를 리턴한다고 하자. 그러면, 리스트가 {A,B, 3, 5} 일때 값을 2를 리턴해야 한다. 이때에 조건으로 숫자일때에는 값을 증가시키고, 숫자가 아닐때에는 값을 증가시키지 않는 방식을 취한다.

'Courses > `2012 AI' 카테고리의 다른 글

composite 실습  (0) 2012.05.07
Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01

4. Resolution Theorem Proving

 

 

 - Resoulution by Refutation ( 반증에 의한 논리 융합)

 

 Resoulution Refutation(도출 반박) 은 사실이라고 알려진 논리와 공리를 부정하는 Goal을 설정한후, 이 것이 모순됨을 보여주어 논리가 true 임을 증명하는 방법이다. 이 증명은 아래의 순서를 따른다.

 

1) 전제나 공리를 clause form으로 둔다.

2) 증명하고자 하는것을, 부정하여 공리 집합에 추가한다.

3) 이 clause form들을 같이 도출하여, logically followed(논리적으로 따라오는) 새로운 clause 를 생성한다.

4) 증명하고자 한것을 부정한것과, 최후에 만들어진 clause를 비교하여, 이들이 empty clause를 생성하면, 증명하고자 하는

   것은 true가 된다.

 

순서만 들어서는 굉장히 햇갈릴 것이다. 하지만 우리는 2장에서 inference rule을 할때에 이미 resolution을 어떻게 사용하는지에 대해서 보았다. 그런데, 한가지 이해가 안가는 말이 있을 수 있다. Clause form 이라는게 무엇일까 ? 이는 흔히 우리들이 ∧ 와 ∨등으로 표현하는 식을 말한다. 예를들어, '말은 동물이다.' 라는 것은 horse(X) -> animal(X) 라고 쓸수 있지만, 이를 clause form으로 고치게 되면,  -horse(X) ∨ animal(X) 이다. 그렇다면 공리를 clause form으로 바꾸는 순서에 대해서 알아보겠다.

 

1) 먼저, 모든 logical connective 인 -> 와 <-> 를 제거 한다.

 

     a <-> b   =  (-a ∨  b) ∧ (-b ∨ a)

     a -> b = (-a ∨ b)

 

2) 부정으로 묶인 scope (괄호) 를 제거한다.

 

  - (a ∧ b)  = -a ∨ -b

 

3) 서로 같은 이름을 가진 변수들이 자신들의 영역에서만 고유하도록 바꿔준다.

 

  (∀X) a(X) ∨ (∀X)b(X)  =  (∀X) a(X) ∨ (∀Y)b(Y)

 

4) 모든 한정자를 왼쪽으로 옮겨서 penex normal form으로 만들어 준다.

5) skolemization을 이용해서 모든 existentail quantifier (∃) 를 없애 준다.

    (ex. ∃X horse(X) 를 skolemization 하게 되면 hore(Maxim)이 된다.

           (∀X)(∀A)(∃B)(∀C)(method(X,A,B,C)) ⇒   (∀X)(∀A)(∀C)(method(X,A,f(X,A),C))  )

6) 모든 universal quantifier를 떼어내 버린다.

7) 모든 표현을 (식) ∧ (식) 의 형태로 고친다.

8) 각각의 ∧로 구분된 식들은 하나의 clause form이 되고, 이들을 다시 rename 하여 사용한다.

 

 

아래의 예제를 보면서 이해해 보도록 하자.

 

 

 

 

 

 

'Courses > `2012 AI' 카테고리의 다른 글

Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01
Calculus Introduction  (0) 2012.05.01

3. Unification (단일화)

 

  1차 술어 논리의 문장 P와 Q가 있다고 해보자. 이 두개의 문장에 있는 각 변수들을 서로 match 시키는 작업을 Unification이라고 한다. 예를들어, ∃X friend(maxim,X) 라는 predicate sentence가 있을때, 이를 unification을 하게되면 friend(maxim,jim) 이 된다. 이때에 도메인에는 maxim의 친구 목록중에 jim이 존재 해야한다. 그리고 이를 {jm/X} 로 표시할 수 있다. 이것은 X를 jim으로 바꿔 주었다는 뜻을 가진다. 좀더 예제를 들어보자. plus(X,Y,Z) 라는 sentence가 있다고 해보자. 여기에 {5/X,3/Y,2/Z}를 적용 시키면 plus(5,3,2)가 되고, 결과값은 10이 된다. 여기에서 숫자(5,3,2)들은 각각 X,Y,Z의 substitute라고 하고, X,Y,Z는 original expression 이라고 한다. 이처럼 단일화를 할때에는 아래의 룰을 따른다.

 

1. Constant (상수) 는 Variable(변수) 의 substitute(대리자)가 될 수 있다.

2. Constant는 다른 것으로 바뀔 수 없다. (대리자를 통한 치환을 할 수 없다.)

3. Variable은 해당 variable을 포함하는 대리자와  unify 될 수 없다. (ex. unify(X, p(X)) is wrong

4. match를 하려는 predicate sentence에는 unify를 통한 변화를 모두 적용 시켜 줘야 한다.

   (ex. plus(X,Y,Z)  와 minus(X,R,T) 가 있을때 {5/X} 를 통해 plus(5,Y,Z)로 바꿔주었다면, minus(5,R,T) 로 역시 변환 해야한다.)

 

 

그리고 unify 룰을 서로 합성 시키는 것이 있는데, 이를 composition(합성) 이라고 한다. 각 단계별로 나오는 unification method 를 합성시키는 것이다. 예를들어 단계별로 나오는 method가 

 

 

{X/Y, W/Z}, {V/X}, {a/V, f(b)/W} 

 

라면   {a/Y, f(b)/Z} 로 composition결과를 만들어 낼 수 있다.

 

그렇다면 이제 위에서 알아본 모든 방법을 가지고 실제 예제를 unification 해보겠다. 아래의 예제를 통해, unify method를 알아내는 방법을 익히도록 하자.

 

unify( (parents X(father X)(mother tom), (parents tom(father tom) Y) )는 차례대로 천천히 unify해 나간다. 2개의 sentence를 앞에서부터 비교하여, 서로 같은 부분을 떼어내어 따로 unify를 하고, 다른 부분은 서로 같게 고칠 수 있으면, 고치고 그렇지 않으면 한쪽에 모두 몰아 넣는다.

 

(1)

 

(parents X(father X)(mother tom)

(parents tom(father tom) Y)           의 첫번째 공통점은 parents 이다. 그러므로 이를 따로 unify를 진행한다.

 

unify(parents, parents) 을 아무러 method없이 떼어내는데 성공했다.

 

 

 

(2)

 

X(father X)(mother tom)

tom(father tom) Y            을 다시 unify하려고 보니, X와 tom이 서로 매치가 된다. 상수는 바꿀 수 없음로 X를 변환한다.

 

 unify(x,tom)이 분리 되었고, 이를 통해 

{tom/X} method가 도출되었다.

 

메서드가 구해졌으니, 이를 남은식에 모두 적용 시킨다. X 는 tom으로 치환된다.

 

(3)

 

(father tom)(mother tom)

(father tom) Y                 을 unify 하니, father 와 뒤의 상수 가 같은 형태 이다. 그러므로 이를 분리 하는데 먼저

 

unify(father tom, father tom) 으로 분리 되고, 다시 한번 분리 되어

 

unify(father, father) 과 unify(tom,tom) 이 된다.  역시, 메서드의 사용 없이 분리가 완료 되었다.

 

 

(4)

 

mother tom

Y                마지막이다. Y와 mother tom은 match 되어야 하므로,

 

unify(mother tom, Y) 로 unify되고,

{mother tom/Y} method가 도출된다.

'Courses > `2012 AI' 카테고리의 다른 글

Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01
Calculus Introduction  (0) 2012.05.01

2. Using Inference Rules to Produce Predicate Calculus Expressions

 

 

 -  Inference Rules

 

 

 

    기존에 주어진 추론을 통해 주어진 명제의 true,false를 가리는 것을, Inference Rule 이라고 한다. 아래의 예제를 보자

 

 "Maxim will die" 라는 문장을 아래의 주어진 statement 들로 부터 증명하라.

 

 Maxim is a horse

 All horses are animals

 All animals will die

 

therefore. Maxim will die

 

이처럼, 주어진 3개의 명제로부터, 새로운 1개의 명제를 증명하였다. 이같은 과정을 추론이라고 한다. 이를 predicate calculus로 나타내면 아래와 같다.

 

 horse(Maxim)

 ∀X (horse(X) ⇒ animal(X))

 ∀Y (animal(Y) ⇒ die(Y))

 

therefore. horse(Maxim) ⇒ die(Maxim)

 

이를 다시 표현하면,

 

 horse(Maxim)

 -horse(X) ∨ animal(X)

 -animal(Y) ∨ die(Y)

 

이다. 이것을 Resolution 에 의해 정리하면 아래표와 같게 된다.

 

 

Figure 1. Resolution

 

  추론 규칙은 sound 와 complete 의 2가지로 평가된다. 우선 sound는, 생성된 문장이 논리적으로 합당한 경우, 사용된 추론 규칙을 sound(정당) 하다고 한다. 예를들면, P와 P⇒Q 가 domain I 의 범위내에서 둘다 true일 때, 'modus ponens' 추론 규칙은 Q또한, true라는것을 알 수 있게 해준다  그리고 complete(완전) 은, 존재하는 모든 문장들이 추론규칙에 의해 논리적으로 합당하게 생성 될 수 있는 경우 추론규칙을 complete(완전) 하다고 한다. 아래는 사용 할 수 있는 추론 규칙에 대한 것이다.

 

- modus ponens : 만약 sentence P와 P ⇒ Q 가 참이라면, modus ponens 은 우리에게 Q가 참임을 암시한다.(추론한다.)

- modus tollens : 만약  P ⇒ Q가 참이고, Q가 거짓 이라면, 우리는 P가 거짓 이라는 걸 알 수 있다.

- and elimination : P ∧ Q가 참이면, P와 Q둘다 참이라는 것을 알 수 있다.

- and introduction : P와 Q가 참이면, P ∧ Q 가 참이라는 것을 알 수 있다.

- universal instantitation : p(X)로 표현된 식은, X의 도메인에 포함된 a로 치환한 p(a)로 표현할 수 있다.

'Courses > `2012 AI' 카테고리의 다른 글

Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01
Calculus Introduction  (0) 2012.05.01

1. Calculus Introduction

 

  우리는 이번 단원에서 두가지의 calculus 를 알아 볼 것이다. Predicate Calculus(명제 논리, 명제 계산) 과 Predicate Calculut(술어 명제, 술어 계산) 의 2가지 이다. 이들은 둘다 모든 언어의 시초라고 할 수 있다.

 

 

 - Propositional Calculus (명제 논리)

  

  Propositional Calculus (명제 논리) 는 참 또는 거짓을 갖는 문장이다. 이것은, 기호, 문장, 의미 로 표현 할 수 있다. 예를 들면 'It is sunny' 라는 문장이 있다고 해보자. 하나의 언어를 하나의 기호로 정의하는 첫 단계를 Symbol (기호) 라고 한다. It is Sunny 라는 문장은 symbol로 변환되어 P 라고 하자. 그렇다면 지금 바깥이 화창하다면 P는 True가 되는 것이고, 화창하지 않다면 False가 되는 것이다.  그렇다면 It is Sunny 라는것은 문장(sentence)이고, P는 기호 (symbol), 그리고 참 거짓은 의미(semantics) 가 되었다. 그리고 이렇게 기호가 된 문장들은 아래의 기호들로 서로의 관계를 표현 할 수 있다.

 

   ∧ -   Conjunct 로 흔히 논리곱이라고 하며 'AND'라고도 표현한다. (ex. -P ∧ P = false) 

   ∨ -   Disjunct 로 흔히 논리 합 이라고 하며 'OR'라고도 표현한다. (ex. P ∨ -P = true) 

   ⇒ -   Implication 으로 논리 함축  이라고 한다. P ⇒ Q 라는 표현식이 있다면, P는 premise(전제) 또는,

            antecedent (선행사)라고 하며 Q는 Conclusion (결과) 라고 한다.

 

 또한 명제 논리는 항등법칙(Equivalences)를 갖고 있는데, 이는 아래와 같다. (여기서 -P는 negation P 를 뜻한다.)

 

 - ( -P) = P

(P ∧ Q) = ( -P ⇒ Q)

(P ⇒ Q) = ( -P ⇒ -Q)

- (P ∨ Q) = ( -P ∧ -Q)

- ( P ∧ -Q) =  ( -P ∨ -Q)

(P ∨ Q) =  (Q ∨ P)

(P ∧ Q) = (Q ∧ P)

((P ∧ Q) ∧ R) = (P ∧ (Q ∧ R))

((P ∧ Q) ∨ R) = (P ∨ R) ∧ (Q ∨ R)

 

 

- Predicate Calculus (술어 논리)

 

 

Predicate calculus (술어 계산) 은 인공지능 언어이다.  술어 논리 라고도 하는 이 것은 형식 언어이다. 1차 술어 논리는 아래의 3가지 요소에 의해 구성된다.

 

1) 구성 규칙 - 반복을 통해 잘 구성된 (well-formed) 논리식을 정의한다.

 

2) 변형 규칙 - 정리를 증명하기 위한 추론 규칙

 

3) 이를 뒷받침하는 비교의 기준 과 추론 방법

 

술어 논리 에서는 '한정자 (Quantifier)'가 변수에만 적용 되고, 술어나 함수에 대해서는 허용하지 않는 경우 이를 일차 술어 계산 이라고 한다. 예를들어 ∀x P(x) 의 경우엔 변수에 한정자가 적용된 예이다. 하지만, ∀P P(x) 의 경우엔 술어부호 P에 한정자가 적용 되었으므로, 일차 술어 계산에서는 허용하지 않는 문장인 것이다. 대부분의 논리적인 표현은 일차 술어계산으로 모두 나타낼 수 있으므로, 인공지능 언어에서는 대부분 일차 술어 계산에 근거하고 있다. 특히, 일차 술어 논리는 집합 이론 전부와 모든 수학을 형식화 하기에 충분히 강력하다.  

 

 명제 논리에서는 각 P와 Q는 한가지의 명제밖에 담지 못했다. 하지만, 술어 논리에서는 각 성분 사이의 관계에 대해 정의 할 수가 있게 된다. 예를들어 'Tom loves Lissa' 라는 문장이 있다고 했을때, 술어 논리는 Top과 Lissa의 관계를 표현하는 love를 이용하여 'love(Tom, Lissa)' 와 같이 표시 할 수 있다. 이처럼 symbol을 문장으로 표현할 수 있는데, 이것은 소문자 대문자 상관 하지 않고 알파뱃과 숫자를 포함 할 수 있지만, 숫자로 시작해서는 안되고, 띄어쓰기와 알파뱃이 아닌 문자는 사용 할 수 없다. (일반적으로 띄어쓰기 대신 언더바 ' _ ' 를 사용한다.) 다시 정리 해보자면 아래와 같다.

 

 1) 소문자, 대문자 상관없이 영문 알파뱃.

 

 2) 숫자 사용 가능 ( 0, 1, .... , 9)

 

 3) 띄어쓰기대신 언더바  '  _  ' 사용가능

 

'Q09M_Z' 와 같은 것은 올바른 symbol의 표현법 이지만, #, %, @ 등과 같은 것이 들어가거나 '9pop' 와 같이 숫자로 시작하는 문장등은 사용해서는 안된다.

 

  좀더 정확히 하자면, 술어 논리에는 다양한 symbol 들이 존재 하는데, 이들마다 이름을 쓸때 지켜야할 규칙이 있다.

 

1) Constant Symbol 은 '상수' 로써, 소문자로 시작 해야 한다.(ex. likes(monkey, banana)  에서 monkey와 banana는 상수)

 

2) Variable Symbol 은 '변수' 로써, 대문자로 시작 해야 한다. (ex. father(X,tom) 여기서 X는 변수)

 

3)  Function Symbol 은 ' 함수' 로써, 소문자로 시작 해야 한다. (ex. 위에서의 likes나  father와 같이)

 

 

 그리고 앞에서 언급했듯이 술어 논리에는 '한정자(quantifier)' 라는게 붙을 수 있다. 한정자에는 2가지 종류가 있는데 universal quantifier 인 ∀ 와, existential quantifier인 ∃ 가 있다. ∀X likes(X,ice_cream) 은 아이스크림을 좋아하는 모든 X는 이라는 뜻을 갖는다. ∃Y friends(Y,Jim) 이라는 것은, 짐이라는 친구를 가진 어떤 Y는 이라는 뜻을 갖는다.  이들은 아래의 룰에 따른다.

 

1) -∀X P(Y) ≡  ∃X -P(X)

2) -∃Y P(Y) ≡  ∀Y -P(Y)

3) ∀X (p(X) ∨ q(X)) ≡ ∀X p(X) ∨ ∀ Y q(Y)

4) ∃X (p(X) ∧ q(X)) ≡ ∃X p(X) ∧ ∃ Y q(Y)

'Courses > `2012 AI' 카테고리의 다른 글

Predicate, Clause form 실습  (0) 2012.05.07
LISP  (0) 2012.05.01
Resolution Theorem Proving  (0) 2012.05.01
Unification  (0) 2012.05.01
Using Inference Rules to Produce Predicate Calculus Expressions  (0) 2012.05.01
Calculus Introduction  (0) 2012.05.01

+ Recent posts