3. 지식 표현과 추론- 술어 논리

술어 논리

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

 

술어

: 문장의 서술어에 해당.

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

 

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

• 존재 한정사: 어떤
• 전칭 한정사: 모든

 

함수: 주어진 인자에 대해서 참, 거짓이 아닌 일반적인 값을 반환.

술어나 다른 함수의 인자로 사용가능.

 

항: 함수의 인자가 될 수 있는 것

ex) 개체상수, 변수, 함

 

 

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

: 술어기호의 인자로 사용될 수 있는 객체나 대상만을 변수화할 수 있고, 

이들 변수에만 한정사를 쓸 수 있도록 한 술어논리

예)

 

 

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

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

예) 

 

술어 논리의 추론

• 술어 논리식의 CNF로의 변환 과정
  1. 전칭 한정사와 존재 한정사를 논리식의 맨 앞으로 끌어내는 변환
  2. 전칭 한정사에 결합된 변수
  -> 전칭 한정사를 없애고  변수는 그대로 남긴다.
  3. 존재 한정사에 결합된 변수
  ex) 어떤 y라면 변수 y는 f(x)로 바꿔야 한다.
  -> 어떤이기 때문에 상수로 바꾸면 안됨.
  그게 아니라면 상수 c로 바꾸면 됨.
  * 스콜렘 함수: 존재 한정사에 결합된 변수를
  해당 술어의 전칭 한정사에 결합된 다른 변수들의 새로운 함수로 대체
  -> 존재 한정사를 없애고 변수를 상수나 함수로 변경

s(x)를 스콜렘 함수라고 함

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

 

 

술어논리로 증명하기

 

1. 증명할 문장에 부정을 취한다 
-> 모순임을 보여 증명하기 위해

2. 각 문장을 논리합 형태로 변환하기

3.  각 문장마다 변수의 표준화 하기 

4. 논리 융합을 통해 모순 이끌어내기

 

Horn절

: 논리식을 논리합의 형태로 표현할 때, 긍정인 리터럴을 최대 하나만 허용

Prolog

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

백트랙킹을 이용하여 실