[인공지능] 8~9. First-Order Logic(FOL)
1. Syntax and Semantics
: propositional logic, 명제논리학은 이 세상의 모든 문제를 propositional symbol로 나타내고 오직 true/false의 값만 가진다. 따라서 이 세상에 많은 object들을 표현하기엔 부족한 면이 있다. (lack the expressive power)
우리가 자연어의 문법을 살펴보면, 대부분의 elements들이 명사와 명사구로 object를 나타내고, 동사나 동사구로 object간의 relation을 나타낸다. 그리고 이 relation중의 일부는 어떤 input이 주어졌을 때 하나의 value를 내뱉는 function(object의 1:1 관계)이기도 하다.
First-order logic은 이 세상엔 object와 이들을 연결하는 relation으로 이루어진다고 가정한다. 그렇기 때문에 PL에 비해 FOL이 우리의 일반적인 상식들을 나타내기에 좋다.
1) Syntax
① symbol : FOL의 가장 기본 문법 요소
- object (=constant symbols)
- relations(=predicate symbols : 서술 symbol) - true나 false를 return하는 funtion
- function (=function symbols) - 어떤 value(symbol)을 return
② term : object를 logical expression으로 표현한 것
- complex term : function symbol과 그에 알맞는 arguments로 이루어진 term
- variable : 그 자체로 term, function의 인수 역할도 함
- constant (ground term임)
* ground term : variable이 없는 term
③ atomic sentence(= atom) : predicate symbol로 이루어짐. complex term을 arguments로 가질 수 있음
④ 더 복잡한 complex sentence를 만들기 위해서는 propositional calculus와 마찬가지로 syntax와 semantics를 기반으로 여러가지 logical connective를 사용해야 한다.
2) Semantics
- equality symbol : First-order logic에서 atomic sentence를 만드는 방법엔 여러가지가 있다. 두 개의 term이 같은 object를 나타낸다는 사실을 equality symbol을 통해 나타낼 수 있다.
- predicate symbol에 의해 정의되는 relation이, argument로 표현되는 object간에 유지된다면 이때의 Atomic sentence는 true이다.
- objects and interpretation
: first-order logic의 model에는 objects와 interpretation의 set이 존재한다. interpretation은 object와 symbol을 mapping 해주는데, 이를 통해 constant symbol이 어떤 objects를 지칭하는지, predicate symbols이 이 objects간의 어떤 relation을 지칭하는지, function symbols이 이 object 간의 어떤 funtions을 지칭하는지를 알 수 있다.
- Propositional logic과 마찬가지로, 모든 가능한 모델에 대해서 entailment, validity 등등의 개념들을 정의할 수 있다.
3) Universal Quantifiers
: "every" 를 뜻하는 quantifier. ∀x P의 꼴로 나타낸다. 이 문장의 뜻은, 모든 object x에 대해 P가 항상 true라는 뜻이다.
좀 더 엄밀히 말해보자면, ∀x P는 Extended interpretation으로 가능한 모든 경우에 P가 참이라면, 주어진 모델에 대해 ∀x P가 true이다. extended interpretation는 x가 가질 수 있는 값의 범위를 지정한다.
예를 들어서 ∀x King(x) ⇒ Person(x)는 모든 x에 대해, x가 king이라면 x는 사람이라는 문장을 나타낸 것이다
∀x King(x) ∧ Person(x) 는 모든 x는 king이거나 person이다. 라는 뜻으로 false이다. (x는 물건일수도, 왕이 아닌 사람일 수도 있다)
(이 때 x는 variable이다)
4) Existential Quantifiers
: "some"을 뜻하는 quantifier. ∃x P의 꼴로 나타내며, 어떤 object x에 대해 P가 true라는 것이다. 즉, P가 true인 x가 적어도 한 개 존재한다는 이야기이다.
좀 더 엄밀히 말하면, 적어도 하나 이상의 extended interpretation에서 p가 true이면, ∃x P가 그 model에서 true이다.
∃x Crown(x) ∧ OnHead(x, John) : 어떤 x가 왕관이고 John이 그 왕관을 쓰고 있다.
∃x Crown(x) ⇒ OnHead(x, John) : 어떤 x가 왕관이라면 John이 그것을 쓰고있다
: x가 왕관이 아니라면 전제가 거짓이 되어 문장이 항상 true가 되므로 사실 별 정보를 담지 못한다. 그래서 existential quantifier과 ⇒ 가 같이 쓰이면 별로 도움이 안된다. (왕관인데 안쓰고 있을 때만 false)
5) Variable Scope : 각 quantifier가 어느 범위까지 영향을 미치는가.
-> 앞에 있는 애부터 해석해나가면 된다.
: 모든 x는 자신이 좋아하는 y가 존재한다. (x1 -> y1 , x2 -> y2...)
: 어떤 y는 모든 x가 좋아한다. (x1, x2 ... -> y1)
또한 서로 상관없는 object를 가리키지만 variable의 이름이 같은 경우가 있는데, 이 경우 헷갈리지 않게 변수명을 바꾸어 준다.
: 모든 x는 왕관이거나 어떤 y는 richard의 brother이다.
6) De Morgan's Rule for Quantifiers
: ∀는 conjunction(논리곱/and), ∃는 disjunction(논리합/or) 이므로 그 애들과 마찬가지로 드모르간 법칙이 성립한다.
-∀x P가 false 다 ! -> P가 false인 x가 존재한다!
-∃x P가 false이다! -> P를 만족하는 x가 없다! -> 모든 x에 대해 not P이다.
2. Examples
1) Wumpus World 를 FOL로 나타내보자
우선 가능한 행동들, predicate symbol에는 Forward, Shoot, Grab, Climb, Turn(Right), Turn(Left)가 있다
또한 모든 t에 대해서 wumpus는 1,3에 존재한다
모든 x,y,a,b 에 대해 Adjacent([x,y],[a,b])는 x가 a와 같고, y가 b-1, b+1이거나 y가 b와 같고 x가 a-1 또는 a+1라는 이야기다. 즉 기준점 [a, b]에 대해 [x, y]가 인접하다는 이야기이다.
그래서 모든 s에 대해 s가 Breezy하면, 즉 바람이 불면, s와 인접한 r에 대해 함정이 있는 r이 존재한다는 이야기다.
PL로 나타낼 때엔 모든 칸에 대해 일일히 다 정의를 해줬어야 했는데 FOL을 이용하니 모든 s에 대해~로 표현이 가능해졌다.
2) 자연어를 FOL로 나타내보자.
"법에 따르면 미국인이 미국의 적국에 무기를 파는 것은 범죄이다. Nano는 미국의 적국인데 미사일을 가지고 있고, 이 모든 미사일은 Colonel West라는 미국인이 팔았다."
1. ∀x,y,z American(x) ∧ Weapon(y) ∧ Sell(x,y,z) ∧ Hostile(z) ⇒ Criminal(x)
2. Enemy(Nano, America)
3. ∃x Owns(Nano, x) ∧ Missile(x)
4. ∀x Missile(x) ∧ Owns(Nano, x) ⇒ Sell(West, x, Nano)
5. American(West)
∀x Enemy(x, America) ⇒ Hostile(x)
∀x Missile(x) ⇒ Weapon(x)
따라서 Criminal(West)
(참고로 quantifier가 없는 경우에는 ∀가 생략되었다고 보면 된다)
3. Instantiation , 추론
1) Universal Instantiation (UI)
: FOL문장에서 Universal Quantified된, 즉 ∀가 붙은 variable은 그냥 ground term(변수 없는 term)으로 치환해도 성립한다.
예를 들어 Subst(θ, α) 는 sentence α에 θ라는 substitution, 대입을 한다는 것을 나타내는 것이다.
그래서 결론적으로 이렇게 바꿀 수 있다.
만약 모든 v에 대해 sentence α가 true라면, α라는 문장에서 ν라는 variable 대신 ｇ라는 ground term을 대입해도 true이다.
2) Existential Instantiation
: FOL 문장에서 ∃가 붙은 variable은 KB에 한 번도 쓰이지 않았던 constant symbol ｋ로 치환해도 문장이 성립한다.
이 새로운 Symbol을 Skolem contant라고 부른다. 그래서 Existential instantiation은 Skolemization의 특수한 케이스에 해당한다.
Universal Instantiation은 여러 번 적용해서 계속해 다른 새로운 문장을 만들어낼 수 있다. 그러나 Existential Instantiation은 딱 한 번만 적용될 수 있다. 적용되고 나면 기존 문장은 사라진다.
위 두가지 추론 규칙을 통해 우리는 문장에 있는 variable과 quantifier을 없앨 수가 있다. 그 두가지를 모두 없애면 PL과 같아진다.
3) Propositionalization : 명제화
: existentially quentified sentence는 하나의 instantiation으로 바꿀 수 있고, universally quantified sentence는 모든 possible instantiation의 집합으로 대체할 수 있다. 따라서 ground atomic sentence를 하나의 propositional symbol로 본다면, 이제 Knowledge Base는 하나의 "명제"가 된다.
quantified sentence들을 이 추론 규칙을 통해 nonquantified sentence로 바꾸면, 앞서 말했던 것 처럼 First-order inference를 propositional inference로 만들 수가 있다.
- Analysis of Propositionalization
그러나 문제가 있다! 만약 Knowledge base에 function symbol이 존재한다면?? ground-term subtitution의 가능성이 무한히 많아진다!
예를 들어보자. f(x), x라는 function symbol에서 x에 f(x)를 대입하면 f(f(x))=f(x), ... 이런식으로 무한하게 많은 SUBSET이 생겨나게 된다.
만약 어떤 문장이 FOL로 만들어진 knowledge base로부터 Entail될 수 있다면, 명제화된 knowledge base의 유한한 부분 집합에서 그 문장을 만들어내는 어떤 증명이 있었다는 것이다. 즉 FOL KB에서 entail 되었다면, Finite subset 안에 proof가 되어야 한다.
처음에 constant symbol을 가지고 있는 모든 instantiation을 생성해낸 다음, term의 depth(괄호 쳐진 횟수)가 1 , 2, ... 인 모든 term을 계속 탐색하다보면 언젠간 entail 된 문장까지 만들어 낼 수 있다. 그러면 증명을 할 수 있다. 탐색하다가 entail된 그 문장을 찾았다면 true를 반환하고, 못 찾았으면 nesting level을 한단계 더 증가시킨다.
그러나 이 방법은 어떤 문장을 entail할 수 있다는 것을 알 수 있을 때만 쓸 수 있다. 만약 이 sentence가 not entailed된다면?? 무한 loop가 돈다면?? 우리는 이 loop가 무한히 도는 동안에는 entail 되는데 아직 못 찾은 건지, 아니면 entail되지 않는 것인지 알 수가 없다. 따라서 FOL에서 Entailment에 대한 문제는 "Semidecidable" 하다. 모든 entailed sentence에 대해서 yes를 내뱉는 알고리즘은 있지만, 모든 nonentailed sentence에 대해서 no를 내뱉는 알고리즘이 없다.
4. Unification
1) Generalized Modus Ponens
: Generalized Modus Ponens는 Modus Ponens의 lifted version이다. 원래 Modus Ponens는 value가 없는 ground propositional logic에서 적용되었던 것인데 이것을 first-order logic에서 적용할 것이다. 이 때 Variables은 모두 universally quantified 되었다고 가정한다.
어떤 atomic sentences pi, pi', q가 있다고 하자. 모든 i에 대해 Subst (θ, pi') = Subst(θ, pi)를 만족하는 substitution θ가 존재한다면, 다음이 성립한다.
뭔소리냐 하면, 참/거짓이 알려진 어떤 문장 n개 (p1'~pi')가 있는데, 이 문장을 이용해서 q라는 문장의 참 거짓을 판별하고 싶다. 그러나 지금은 안의 변수 자리에 각기 다른 값들이 들어가 있어서 활용을 할 수가 없다. 이 때 우리가 알아야 하는 것은 (p1~pi)이다. 따라서 문장 pi' 또는 pi에 어떤 subst를 적용해서 pi'와 pi가 같은 문장이 되도록 만들어 주는 것이다. 그렇게 같은 문장이 되면 q의 진리값을 구하는데 주어진 정보를 이용할 수 있다.
따라서 'p1 , p2, p3 ... pn이 모두 true이면 q이다'라는 문장이 참이라는 사실을 알고 p1'~pi'가 true라는 사실을 아는 상태에서, q sentence에 pi' 와 pi를 모두 같게 만든 그 substitution을 적용했을 때에도 참이 된다는 것이다.
예를 들어 위 사진을 보자. King이면서 greedy한 x는 모두 evil이다.
사람은 john이 king이고, 모든 y에 대해 greedy가 참임을 알기 때문에, john이 evil이라는 사실을 바로 알 수 있다.
그러나 기계가 알아듣게 하는 것은 다른 문제!
P1': King(john)
P2': Greedy(y)
P1 : King(x)
P2 : Greedy(x)
Q : Evil(x)
우리가 알고 싶은 것은 q의 진리값.
우리가 알고 있는 것은 P1', P2' 그리고 P1 ∧ P2 ⇒ Q
Greedy(y) 문장에서 x에 john을 , y에 john을 대입하는 subst가 있다. greedy는 universial quantified sentence이기 때문에 y variable 대신에 어떤 constant symbol을 넣어도 여전히 참이다. 즉 이 subst는 참이다. 이 Subst를 P2와 P2'에 둘 다 적용시켜보면 둘 다 결과적으로 Greedy(John)이 되어 같아진다.
King(John) 과 King(x) 두 문장에 모두 위에서 했던 Subst를 그대로 적용시켜보자. 그러면 두 문장이 모두 King(John)이 되어 같아진다.
P1 ∧ P2 ⇒ Q 이 문장에서 위에서 했던 subst를 그대로 적용시켜보자. 그러면 King(John) ∧ Greedy(John) ⇒ Evil(John) 이라는 문장이 되고, 이 때 king(John)과 Greedy(John)이 모두 true이므로 Evil(John)도 true가 된다.
즉, Q라는 문장에 x/John, y/John 이라는 subst를 적용하면 true가 된다.
2) Unification
: 서로 다른 logical expression을 identical하게 보이도록 만들어주는 substitution을 찾는 과정
unify algorithm은 두 개의 문장을 받아서 둘을 똑같게 만드는 Substitution(Unification)을 return해준다.
* Unify(p,q) = θ where Subst(θ, p) = Subst(θ, q)
p와 q가 어떤 substitution θ에 의해 같아질 때, p와 q의 unify는 θ이다.즉 Unify(p, q)는 p와 q를 같게 만들어주는 substitution을 return한다.
- Standardizing apart : 두 문장에서 서로 관련이 없는 변수인데 이름이 같아 crash가 나는 것을 방지하기 위해 이름 같은 변수들의 이름을 바꿔주는 것을 말한다.
P(x, B)와 P(A, x)를 Unify하면 failure가 뜬다. 왜? x값을 같은 변수로 인식해서 x에 어떤 수를 넣어도 같이질 수 없다고 판단했기 때문이다. 그래서 우리는 둘 중 하나를 y로 바꿔준다.
사실 모든 unifiable한 표현의 쌍들은 가능한 substitution이 매우매우 많다. 그래서 그 중에서도 가장 간단한 unifier를 most general unifier라고 한다. 이게 제일 renaming하고 변수들을 치환하는데 깔꼼하다.
다음은 Unify 알고리즘이다.
5. Forward Chaining Algorithm
- PL과는 다르게 FOL은 variable을 포함할 수가 있다. 그리고 이 모든 variable은 "universally quantified"하다고 가정한다.
- definite clause는 atomic sentence 이거나 antecedent(=premise)가 positive literal들의 conjunction(and)로 연결되고 consequent가 single positive인 implication를 말한다. (원래 꼴은 하나만 positive인 or로 묶인 clause)
- Forward Chainig Algorithm 은 앞에서 나왔던 것과 같다.
이미 알려진 known facts에서 시작해서 모든 premise가 satisfied라면 그 문장의 conclusion을 known fact에 추가해준다. 이 방법을 반복하다가 query에 대한 답을 찾거나 더이상 추가할 new fact가 없으면 끝난다.
조심해야 할 것은, 여기서 "new" fact란, 단지 이미 알려진 fact에서 변수 이름만 바뀐 것이어서는 안된다. 변수의 이름을 제외하고 다른 것들이 다 동일한 경우에는, 그 문장은 같은 문장이다. (단지 renaming 된 것 뿐)
알고리즘은 아래와 같다.
자 그럼 우리가 아까 풀었던 범죄자 문제를 가져와보자.
1. American(x) ∧ Weapon(y) ∧ Sell(x,y,z) ∧ Hostile(z) ⇒ Criminal(x) (∀x,y,z 생략)
2. Enemy(Nano, America)
3. Owns(Nano, M1) ∧ Missile(M1) (어떤 값이 있다 했으니 어떤 값으로 치환하여 quantifiers를 없애버린다)
4. Missile(x) ∧ Owns(Nano, x) ⇒ Sell(West, x, Nano)
5. American(West)
Enemy(x, America) ⇒ Hostile(x)
Missile(x) ⇒ Weapon(x)
Criminal (West) ? - query
------
자 먼저 2. Enemy(Nano, America) 이라는 fact로부터 Enemy(x, America) ⇒ Hostile(x) 식을 찾는다. 그리고 식의 x에 Nano를 대입해보자. 그러면 implication을 만족하기 때문에 Hostile(Nano)를 KB에 추가한다.
다음으로는 Missile(M1)이라는 fact와 Owns(Nano, M1)이라는 fact로부터 3. Missile(x) ∧ Owns(Nano, x) ⇒ Sell(West, x, Nano) 문장을 꺼내온다. x = M1을 대입하면 Sells(West, M1, Nano)는 true가 되어 KB에 추가한다.
다음으로는 Missile(M1)이라는 fact에서 Missile(x) ⇒ Weapon(x) 식을 꺼내온다. x=M1을 대입해 Weapon(M1)이 true임을 밝힌다.
마지막으로 American(x) ∧ Weapon (y) ∧ Sells(x, y, z) ∧ Hostile(z) ⇒ Criminal(x)에서 x = West, y = M1, z=Nano를 대입하여 Criminal(West)를 밝혀낸다.
최종적으로 찾은 criminal(west)가 바로 query이고, 이것은 KB에 의해 entail 된다.
- Analysis
① 모든 inference가 generalized Modus Ponens에서 비롯되었으므로 당연히 Sound 하다.
② Knowledge Base가 definite clause로 구성되었을 때, complete하다.
( function symbol이 없으면 ground term의 개수 유한 -> ground fact도 유한 -> complete)
( function symbol이 있으면 ~ 증명 나중에~ )
③ goal과 관련 없는 fact까지 전부 탐색해서 비효율적이다.
6. Resolution Algorithm
1) Resolution Rule for First-order Logic
* Binary resolution rule
- PL에서 쓰이던 resolution rule을 first-order clauses에서 쓸 수 있게 lifted된 것
- 두 clauses가 각각 standardized apart되어서 어떠한 공통인 variable도 없을 때, complementary literall을 가지고 있다면 resolution을 사용할 수 있다.
- FOL에서 Literal이 complementary 하다는 것은, 어떤 한 literal이 다른 literal과 unify되는 것을 말한다.
보이는 것처럼 일단은 standardized apart 되어야 하고, 합쳐서 없앨 수 있는 것은 unify 되는 두 리터럴이다.
예를 들어 다음과 같은 clause를 보면, Loves(G(x),x)와 Loves(u,v)가 unify하고 서로 complementary 하다. 따라서 u= G(x), v=x를 대입하는 subst를 적용하였을 때, 그 두 리터럴을 빼고 나머지끼리 and 연산으로 합쳐줘도 true이다.
(참고 : PL 에서는 P∧Q∧R∧P=P∧Q∧R이었다.
FOL 에서는 P(x)∧Q(x)∧R(x)∧P(v) 에서 P(x)와 P(v)가 unify 가능하면 없앨 수 있다.)
2) Conjunctive Normal Form
- PL에서도 그랬듯이 이런 resolution을 쓰려면 sentence들이 conjunctive normal form, 즉 CF로 나타나야 한다. Sentence에 있는 variable들은 기본적으로 universally quantified라고 생각해라. Definite clause를 CNF로 바꿔보자.
CNF sentence로 바꿔도 문장은 inferentially equivalent하다.
① Biconditional elimination을 이용해 ⇔ 기호를 다 없앤다 (α ⇔ β) ≡ (α ⇒ β)∧(α ⇒ β)
② Implication elimination을 이용해 ⇒ 기호를 다 없앤다 (α ⇒ β) ≡￢α ∨ β
③ double-negation elimination과 de morgan 법칙을 써서 ￢ 기호를 모두 괄호안으로 넣어준다.
④ Standardize variables : 서로 관련 없는 변수는 다른 이름으로 바꿔준다.
⑤ Skolemize : ∃ 표시 없애기
⑥ Remove universal quantifiers : ∀ quantifiers도 죄다 없애기
⑦ distributivity law를 사용해서 ∧를 괄호 밖으로, ∨을 괄호 안으로 넣어준다.
->원래 문장이 unsatisfiable하면 CNF sentence도 unsatisfiable하다.
예시를 보자. 그냥 쭉 읽어보면 된다.
여기서도 마찬가지로 KB가 α를 entail하는지 보기 위해서는 KB⇒α 가 valid한지 봐야하고, 이는 KB∧￢α 가 unsatistiable 한지 확인해야 한다. 따라서 resolution 알고리즘을 통해 KB∧￢α이 식을 Resolution 했을 때 empty set이 나오는지 안나오는지를 확인하면 된다.
보면 우리가 entail 되는지 안되는지 확인할 query 문의 부정이 R9에 있다. R1~R9가 모두 true라고 가정하고 resolution을 쭉쭉 진행하다 보면 R18에서 empty set이 나오는 것을 알 수 있다. 따라서 R9의 부정문인 Criminal(West)는 KB로부터 entail 된다.
- Completeness of Proof by Resolution (FOL에서 Resolution을 이용한 proof가 Complete한 이유)
