[Knowledge Expression] 논리 2 - 술어 논리

논리

말로 표현된 문장들에 대한 타당한 추론을 위해, 기호를 사용하여 문장들을 표현하고 기호의 조작을 통해 문장들의 참 또는 거짓을 판정하는 분야

술어 논리란?

술어 논리

명제의 내용을 다루기 위해 변수, 함수 등을 도입하고 이들의 값에 따라 참, 거짓이 결정되도록 명제 논리를 확장한 논리

술어

• 문장의 주어 + 서술어 형태에서 서술어에 해당

• 대상의 속성이나 대상간의 관계를 기술하는 기호

• 참 또는 거짓을 부여하는 명제의 기본 형식

• 예

  

술어 논리의 구문

존재 한정사와 전칭 한정사

• 변수의 범위를 고려한 지식을 표현

• 예

  

함수

• 주어진 인자에 대해서 참, 거짓 값이 아닌 일반적인 값을 반환
• 술어나 다른 함수의 인자로 사용

항

• 함수의 인자가 될 수 있는 것
• 항이 될 수 있는 것: 개체상수, 변수, 함수
  1. 개체 상수, 변수는 항이다.
  2. t1, t2, …, tn이 모두 항이고, f가 n개의 인자를 갖는 함수 기호일 때, f(t1, t2, …, tn)은 항이다.
  3. 1과 2에 의해 만들어질 수 있는 것만 항이다.

술어 논리식에 대한 정형식

술어 논리의 종류

일차 술어논리 (first-order predicate logic, FOL)

술어 기호의 인자로 사용될 수 있는 객체나 대상 만을 변수화할 수 있고, 이들 변수에만 전칭 한정사와 존재 한정사를 쓸 수 있도록 한 술어논리

고차 술어논리 (high-order predicate logic)

함수나 술어기호도 변수화할 수 있고, 이들 변수에 대해서도 전칭 한정사와 존재 한정사를 쓸 수 있도록 한 술어논리

+추가

일차술어 논리문과 고차술어 논리문 의 구분법을 단순화하면 다음과 같다.

“술어논리문에서 함수나 술어 기호는 항상 괄호( )를 동반하므로 괄호 앞의 함수나 술어 기호가 상수가 아니고 변수라면 1차 술어논리문이 아니다. “

술어논리에서 어떤 것을 지칭하기 위한 용어(항, term)로서 기호를 이용하는데, 특정 개체(또는 객체, object)에 대해 기호를 사용하여 직접적으로 언급하거나 (예: Mary 나 Tom이라는 사람에 대해 ‘ Mary’ 나 ‘Tom’ 이라는 기호를 사용하여 언급), 아니면 함수기호와 인자를 사용하여 간접적으로 언급할 수도 있습니다(예: Mary 가 Tom의 어머니인 경우 Motherof 라는 함수기호와 Tom 이라는 인자를 이용하여 Motherof(Tom) 라는 용어(항)로 실제의 Mary 를 언급)

그런데 여기서 ‘Motherof’ 와 ‘Tom’은 모두 상수기호입니다. ‘Motherof’는 누군가의 어머니를 나타내는 특정한 함수에 대한 기호로서 사용된 함수상수(function constant) 기호이고, ‘Tom’은 Tom이라는 특정 인물 을 언급하는데 사용된 개체상수(object constant) 기호입니다.) 우리가 지금 다루고 있는 기호논리학(symbolic logic)에서는 이렇게 개체, 함수, 술어를 나타내는데 사용하는 기호 어떤 것이든 특정한 것을 나타내기 위해 사용하는 기호면 모두 다 상수라 합니다. (보통 관습적으로 상수기호와 변수 기호를 구분하기 위해 대문자를 써서 상수를 나타내고, 소문자를 써서 변수를 나타냅니다.)

그런데 1차 술어논리에서는 함수명으로 사용하는 기호나 술어로 사용하는 기호를 변수화하여 문장으로 표현할 수 없다는 것입니다. 함수기호나 술어기호를 변수화해서 문장을 만들면 그 문장은 1차술어논리 체계의 문장이 아니라 고차술어논리 체계의 문장이 되는 것입니다.

예를 들어 아래의 문장에서 F, H, g는 인자를 하나씩 가지는 함수를 지칭하기 위해 사용된 기호인데, F와 H 는 삼각함수 Sin 이나 Cos 함수처럼 특정함수를 나타내는 용어(상수)로서 사용된 상수 기호이고, g는 불특정한 함수를 지칭하는 용어(변수)로서 사용된 변수 기호입니다. 따라서 아래의 문장은 1차 술어논리문은 아닙니다 ( a = b 형식의 문장 표현은 술어논리 문장의 형태인 = (a,b) 의 다른 표현이라고 가정하겠습니다)

위의 문장에서 g(x)를 G(x)로 바꿔 특정 함수를 지칭하는 상수 함수로 바꾸고, 앞의 전칭 한정사 ∃g 를 없애면 1차 술어 논리문이 될 것입니다.

반면, 다음의 문장은 1차 술어논리문입니다

술어 논리의 지식 표현

술어 논리의 추론

술어논리식의 CNF(논리곱 정규형)로의 변환 과정

• 전칭 한정사와 존재 한정사를 논리식의 맨 앞으로 끌어내는 변환

• 전칭 한정사에 결합된 변수
  • 임의의 값 허용
• 존재 한정사에 결합된 변수
  • 대응되는 술어 기호를 참으로 만드는 값을 변수에 대응시킴
  • 스콜렘 함수 (Skolem function)
    • 존재 한정사에 결합된 변수를 해당 술어의 전칭 한정사에 결합된 다른 변수들의 새로운 함수로 대체: s(x)
    • 예

정리하면 술어논리식의 CNF로의 변환과정은,

• 전칭 한정사만 존재하는 변수의 경우 논리식에서 전칭 한정사 삭제. 이는 변수에 임의의 값을 허용함을 뜻함.
• 존재 한정사만 존재하는 변수의 경우 대응되는 술어기호를 참으로 만드는 상수 값을 변수에 대응.
• 존재 한정사와 전치 한정사가 함께 사용되는 경우 스콜렘 함수를 변수에 대응.

자세한 변환 과정은 아래와 같다.

1단계: 함의기호 (->) 제거

p -> q는 ㄱp or q 로 변환

2단계: 부정 기호(ㄱ)의 적용 범위 축소

ㄱ(p or q)는 ㄱp and ㄱq로 변환

ㄱ(p and q)는 ㄱp or ㄱq로 변환

ㄱ∀x p 는 ∃x ㄱp로 변환

ㄱ∃x p는 ∀x ㄱp로 변환

ㄱㄱp는 p로 변환

3단계: 변수명 표준화

예를 들어, (∀xP(x)) or (∃xQ(x)) 문장은 (∀xP(x)) or (∃yQ(y))로 변환

(여기서 y는 다른 문장에 나타나지 않는 새로운 변수명)

4단계: 존재 한정사 제거(스콜렘 화)

존재 한정사와 해당 변수를 없애는 과정

• Case 1: 존재 한정사 바깥에 전칭 한정사가 없는 경우
  • ∃yPerson(y)의 문장은 Person(A)로 변환
  • 여기서 A는 다른 문장에는 나타나지 않는 새로운 상수 기호(Skolem 상수)
• Case 2: 존재 한정사의 바깥에 전칭 한정사가 있어서 그것에 의해 한정이 되는 경우
  • ∀x∃y[P(x) and Q(x, y)]의 문장은 ∀x[P(x) and Q(x, S(x))] 로 변환
  • 여기서 S는 다른 문장에서는 나타나지 않는 새로운 함수 기호(Skolem 함수)

5단계: 한정사를 맨 왼쪽으로 이동

모든 전칭 한정사를 순서는 유지한 채 문장의 왼쪽으로 이동.

이런 형태를 prenex from이라 칭함.

예를 들어, p or ∀x q의 문장은 ∀x (p or q)로 변환

6단계: 전칭 한정사를 제외한 나머지 부분을 CNF로 변환

분배 법칙을 사용하여 논리식을 CNF(논리곱 정규형)로 변환

7단계: 전칭 한정사 제거

∀x∀y[p(x) or q(y)]의 문장은 p(x) or q(y)로 변환

단일화 과정

논리융합을 적용할 때, 대응되는 리터럴이 같아지도록 변수의 값을 맞춰주는 과정

술어 논리로 지식의 증명

논리 프로그래밍 언어

• Horn 절

  • 논리식을 논리합의 형태로 표현할 때, ㄱA(x) or ㄱB(x) or ㄱC(x)와 같이 긍정인 리터럴을 최대 하나만 허용

• Prolog

  • Horn 절만 허용하는 논리 프로그래밍 언어

  

  • 백트래킹을 이용하여 실행