论文标题
键入SLD分辨率：逻辑编程的动态键入
Typed SLD-Resolution: Dynamic Typing for Logic Programming
论文作者
论文摘要
逻辑编程的语义基础通常分为两种不同的方法。使用SLD分辨率的操作语义，计算逻辑编程中答案的证明方法以及声明性语义，该语义语义将逻辑程序视为公式及其语义作为模型。在这里，我们定义了一种称为TSLD分辨率的新操作语义，该语义代表键入的SLD分辨率，其中我们包含一个值“错误”的值，该值与运行时类型错误的检测相对应。为此，我们定义了一种新的键入统一算法。最后，我们证明了TSLD分辨率相对于打字声明语义的正确性。
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative semantics, which sees logic programs as formulas and its semantics as models. Here, we define a new operational semantics called TSLD-resolution, which stands for Typed SLD-resolution, where we include a value "wrong", that corresponds to the detection of a type error at run-time. For this we define a new typed unification algorithm. Finally we prove the correctness of TSLD-resolution with respect to a typed declarative semantics.
