逻辑程序始于上世纪70年代初，来源于定理机器证明与人工智能的研究。在逻辑程序30年的发展中，它已经成为了人工智能领域中重要的一个方向，在众多人工智能领域展示着它的价值。逻辑程序语义的研究中重要的一个方面就是否定的处理。处理否定最基本的两种方法是闭世界假定(closed world assumption)和失败即否定原则(negation as failure)。本文所论述的非基有限失败语义，是对于失败即否定原则的研究。在对非基有限失败语义的研究中，抽象解释(abstract interpretation)方法被用于不动点语义的推导。 抽象解释方法是一种用于近似程序语义的通用方法。其核心思想在于构建和联系程序的两个不用的语义：具体语义(concrete semantics)和抽象语义(abstract semantics)，抽象语义是具体语义的近似。抽象解释方法与逻辑程序有着紧密的联系，在逻辑程序语义的研究中有着重要的作用。 有限失败是失败即否定原则中重要的概念，它是指求解一个目标所得到的SLD树是有限且每个分支都是失败的。最先在文献中介绍的用来描述有限失败的语义是(基)有限失败集FF_p(程序P有限失败的基原子集合)， FF_p={A|A是基原子，←A有一棵公平的有限失败SLD树}。 然而这个语义并不能正确描述有限失败。如果我们考虑≈FF，程序之间关于相同有限失败目标集的等价，我们可以看出FF_p不足以区分不等价的程序。即两个程序有相同的基有限失败集，但某个目标在两个程序中关于有限失败的行为并不相同。 因此，一个新的有限失败语义被提出：非基有限失败集合NGFF_p， NGFF_p={A|←A有一棵公平的有限失败SLD树}。 NGFF_p被证明对于有限失败是正确的。接下来一个重要的问题是给出关于非基有限失败的不动点语义。 为了描述有限失败，首先应该尽可能详尽地表达推导过程中得到的SLD树，为此本文首先介绍了Comini提出了一个语义框架：SLD推导语义，这个语义可以对有限SLD推导进行推理。SLD推导语义的基本概念是合式推导集合，合式推导集合是部分SLD树的形式化表示。语义域是collection的构成的完备格，collection是将目标映射到合式推导集合的部分函数，可以看作是一个目标在推导过程中得到的部分SLD树。在此基础上，本文介绍了SLD推导语义中推导的联接、实例化、合取，collection的和、积、实例化、组合、扩展等基本运算符，以及应用这些运算符定义的指称语义、操作语义。然后叙述了语义的几个性质：指称语义和操作语义的等价，自顶向下与自底向上指称的等价，指称的正确性及最小性，指称的AND组合性。 接下来本文介绍了在此基础上发展出来的可观察行为理论。可观察行为在这个框架中被形式化为具体域和抽象域之间的Galois嵌入。其中具体域描述SLD树，抽象域描述我们感兴趣的行为。由可观察行为的概念可定义理想的抽象运算符，当我们用理想的抽象运算符来代替相应的具体运算符，就可以从具体的语义得到相应的抽象的语义。然后介绍了两类重要的可观察行为，它们是满足一定充分条件的可观察行为，摘要并且介绍了它们的性质。第一类可观察行为是标准(perfect)可观察行为，它是一种抽象的操作语义和指称语义都精确的可观察行为。另一类可观察行为是指称(denotational)可观察行为，其中理想条件被放宽。 因为这个可观察行为理论框架只关注有限推导，而为了研究有限失败的性质，我们需要区分有限失败的推导和无限推导的部分答案，因此它不能被用作描述有限失败的性质。为了将可观察行为理论用于处理有限失败，接下来本文介绍了Gori扩展了的SLD推导语义和可观察行为，扩展了的框架可处理无限推导。他将无限推导分为永久无限推导和非永久无限推导两类，给出了与有限失败经典的向下封闭性质相对应的向上封闭性质。在此基础上，得出了用于分析非基有限失败的可观察行为，并且证明它满足一定的充分条件，这些充分条件可以保证抽象语义是精确的。这个语义可以作为一个共连续算子的最大不动点计算出。 本文的工作是对Gori框架中可观察行为的抽象域进行重构。基于有限失败的向一下封闭性质，本文提出了最小生成集的概念，应用最小生成集来表示非基有限失败的原子集。首先给出了最小生成集的定义，用最小生成集对抽象域进行了重构，并且重新定义了其上的序关系。然后本文给出了基于最小生成集的非基有限失败可观察行为，证明了它满足Gori框架中的充分条件，由此得到用最小生成集表示非基有限失败原子集的不动点语义。