비균일 정의역 위에서의 일차 논리 언어의미 부여에 관한 연구

Abstract

논리 프로그램에 대한 '의도적 의미 부여'가 일차 논리 언어를 대상으로 하는 의미 부여에 관한 정의에 부합하지 않을 때가 있다. 논리 프로그램에 관한 의미 부여와 일차 논리 언어에 대한 의미 부여 사이의 괴리를 메우기 위해, 본 논문에서는 '형을 가진' 일차 논리 언어를 제안함과 더불어 그것에 대한 형을 가진 의미부여도 제시하였다. 뿐만 아니라, 절의 집합 S를 만족시키는 형을 가진 허브란드식 의미부여 I*가 없다는 사실은 S를 만족시키기가 불가능 하다는 데 대한 필요충분조건임도 보였다.

sometimes the "intended interpretation" of a logic program is not an interpretation of a first order language. To fill the gap between the interpretation of a logic program and the interpretation of a first order language, we propose a typed first order language and a typed interpretation of it. Together with them it is proved that a set of clauses S is unsatisfiable iff S has no typed Herbrand interpretation I* that satisfies S.

sometimes the "intended interpretation" of a logic program is not an interpretation of a first order language. To fill the gap between the interpretation of a logic program and the interpretation of a first order language, we propose a typed first order language and a typed interpretation of it. Together with them it is proved that a set of clauses S is unsatisfiable iff S has no typed Herbrand interpretation I* that satisfies S.