술어 논리(predicate logic)

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

술어(predicate)

문장의 '주어+서술어' 형태에서 서술어에 해당
대상의 속성이나 대상간의 관계를 기술하는 기호
참 또는 거짓 값을 갖는 명제의 기본형식

존재 한정사 ∃ 와 전칭 한정사 ∀ 사용

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

함수(function)

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

항(term)

함수의 인자가 될 수 있는 것
항이 될 수 있는 것 : 개체상수, 변수, 함수

술어 논리식에 대한 정형식

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

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

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

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

술어 논리식의 CNF로의 변환 과정

1. 전칭 한정사와 존재 한정사를 논리식의 맨 앞으로 끌어내는 변환
2. 전칭 한정사에 결합된 변수(임의의 값 허용)
3. 존재 한정사에 결합된 변수
   • 대응되는 술어 기호를 참으로 만드는 값을 변수에 대응시킴
   • 스콜렘 함수(Skolem function)
     존재 한정사에 결합된 변수를 해당 술어의 전칭 한정사에 결합된 다른 변수들의 새로운 함수로 대체

단일화(unification) 과정

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

논리 프로그래밍 언어

Horn 절

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

Prolog

Horn 절만 허용하는 논리 프로그래밍 언어
백트랙킹을 이용하여 실행