终止逻辑程序的若干类

逻辑程序的终止性质在于选择规则，即在每个分辨步骤中决定选择哪个原子的规则。在本文中，我们根据不同的选择规则对程序（和查询）进行分类。这是一个关于文献中不同方法的调查和统一视图。对于每一类，我们提出了判定该程序是否属于该类的充分条件，对于大多数类别甚至是必要条件。我们研究了六类：若程序对所有选择规则都终止，则称为强终止程序；若程序对仅选择其输入位置足够实例化的原子的选择规则终止，则称为输入终止程序，这些参数在由统一进一步实例化之前不会再被实例化；若程序对仅选择基于适当层级映射受限的原子的局部选择规则终止，则称为局部延迟终止程序；若程序对常用的从左到右选择规则终止，则称为左终止程序；若存在一种选择规则使其终止，则称为存在终止程序；最后，若程序仅具有有限个反证，则称为具有有限非确定性的程序。我们提出了一种从具有有限非确定性的程序转换为强终止程序的语义保持转换。此外，通过统一不同形式化方法并作出适当假设，我们能够在不同类别之间建立形式化层次结构。