Equational disjunctive logic languages

국문 초록 (Abstract)

본 논문은 술어 논리와 등식 논리에 기반을 둔 프로그래밍 언어의 설계와 구현을 다룬다. 이 언어는 완전한 이접 클로즈를 표현할 수 있기 때문에 Prolog 언어와 같은 혼 논리 언어보다 표현력이 강하다. 또한 이 언어에서 는 등식을 표현할 수 있기 때문에 이 언어를 논리 언어와 함수 언어가 결합 된 언어라고 말 할 수 있다. 본 연구에서는 이접 허브란드 E-해석을 이용하 여 이 언어의 모델 이론적 의미를 정의하고, 최소 이접 허브란드 E-모델이 이 언어의 모델 이론적 의미임을 증명하였다. 또한 EP-MPRF이라는 증명 절 차를 정의하고 이 증명 절차의 안정성과 완벽성을 증명하였다. 제시된 언어 의 효율적인 구현을 위하여, 3단계로 구성되는 본 언어의 컴파일 방법을 제 시한다. 첫번째로, 등식 이접 논리 언어의 등식 클로즈를 논리적 클로즈로 변환하기 위하여 등식 이접 논리 프로그램을 평평한 형식으로 변환한다. 두번째로, 앞 단계에서 변환된 프로그램을 MPRF 증명 절차를 이용하여 동등 한 의미의 혼 논리 프로그램으로 변환한다. 세번째로, 앞 단계에서 변환된 프로그램을 MPRF의 공리와 분리 규칙을 효율적으로 구현하기 위하여 확장된 WAM 프로그램으로 변환한다. 실험적 구현을 통하여 본 논문에서 설계된 확장 WAM은 컴파일된 이접 논리 프로그램을 매우 효율적으로 수행함을 보였다.

다국어 초록 (Multilingual Abstract)

We design and implement a programming language that is based on both pred-icate
logic and equational logic. This language is more expressive than Horn logic
languages like Prolog since we can represent full disjunctive clauses. We can also
represent equations, so we can think of this language as an integration of a logic
language and a functional language.
In this research, we define the model theoretic semantics of the language using
disjunctive Herbrand E-interpretation and show that the model theoretic semantics
is the least disjunctive Herbrand E-model. We also propose a proof procedure called
EP-MPRF that is based on Plaisted MPRF and show that it is sound and complete
for the language.
As an efficient implementation for the language, we propose a compilation scheme
composed of three steps. First, an equational disjunctive logic program is flattened to transform equational clauses into logical clauses, yielding a disjunctive logic program.
Second, the proof rules of MPRF are used to convert the disjunctive logic
program into an equivalent Prolog program. Third, this Prolog program is compiled
to a WAM which has been extended to support efficient implementation of the Ax-ioms
and splitting rule of MPRF. The extended WAM has some new registers, new
instructions, and extended environment frame and choice point structures. Experiments indicate the experimental extended WAM executes compiled disjunctive logic programs very efficiently.