论文部分内容阅读
<正> 1.稳固模型和良构指派 首先假定读者已熟悉有关逻辑程序设计的最基本概念,有关详细论述请参阅[3]。 定义1.设P是一Horn逻辑程序(简称Horn程序),B_P是P的Herbrand域.T_P是一从解释I到另一解释T_P(I)的映射,定义为: T_P(I)={A∈B_P|存在P中某子句的实例代换A←A_1,…,A_n,使得{A_1,…,A_n}I}