基于标记逻辑的非单调推理（II）

本文研究不循环ＡＬＰ的说明语义，利用依赖关系的非自反应性，把程序的Ｈｅｒｂａｒａｎｄ基分类成一系列不相交集合，在此基础上，引进多重极限的概念，并证明，不循环程序存在唯一的支持模型，该模型就是程序的ｋ重极限，其中ｋ是程序中自由子句的个数。