一阶逻辑的证明理论与静态分析程序的正确答案，基于证明而非模型的理论计算机科学笔记

理论计算机科学电子笔记48（2001）网址：http://www.elsevier.nl/locate/entcs/volume48.htmlpp. 1–一阶逻辑Gianluca Amato1乌迪内大学数学与信息学院意大利乌迪内摘要在文献[3]中发展的一个逻辑演算的语义框架内，我们对正确答案和正确结果的概念提出了几个扩展，这些扩展可以应用于完全的一阶逻辑。相对于以前的建议，这是基于证明理论，而不是模型理论。我们激励我们的选择与几个例子，我们展示了如何使用正确的答案来重建一个抽象，这是广泛使用的静态分析的逻辑程序，即接地。作为应用的一个例子，我们提出了一个原型的自顶向下的静态解释器的属性的接地工作的完整的直觉主义一阶逻辑。1介绍逻辑编程的最大好处之一，如[20]所述，是它基于可执行规范的概念。逻辑程序的文本被赋予了操作（算法）解释和独立的数学意义，它们在几个方面相互一致问题是操作表达性（旨在指导程序执行流程的能力）往往会模糊声明性的含义。逻辑编程的研究努力在这些相反的需求之间找到一个良好的平衡。统一证明[21]已被广泛接受为解决问题的主要工具之一，并区分没有明确计算工具的逻辑然而，统一证明是一个严重基于证明理论的概念，沿着这条路线进行的研究一直与基于定点语义的传统方法相距甚远。反过来，后者的传统带来了一些重要的成果，关于有效利用霍恩子句作为一个真正的1电子邮件：amato@dimi.uniud.it2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。阿马托2∃编程语言.其中，诸如语义的组合性[10，9]、模块化[6，8]、静态分析[14]、调试[11]等问题已经在此设置中得到解决。将这些结果应用于通过证明理论方法开发的新逻辑语言，如λProlog [23]或LinLog [4]，可能需要至少两件事：• 为这些新语言提供定点语义;• 它概括了大量的概念，这些概念的定义太多地与Horn子句的情况联系在一起。在[3]中，作者提出了一个语义框架，它可以在这样一个分类中是有用的。其主要思想是认识到证明在微积分作为一般对应的SLD决议的积极的逻辑程序。因此，Horn子句逻辑的三种著名语义（操作性、声明性和定点性）可以在这个通用设置中重新表达，并直接应用于所有基于微积分的逻辑语言。经典的抽象，如正确的答案或结果，用于逻辑程序的语义研究，和抽象的静态分析，如接地，可以检索的性质证明。以这种方式表达，而不是指像SLD解决方案的计算过程，他们更容易扩展到其他逻辑语言。然而，[3]中提出的正确答案的定义是基于模型论的思想，即存在性量化公式x.φ的正确答案是x中变量的替换θ，使得φθ为真。当我们试图把这个简单的概念从众所周知的霍恩子句的情况扩展到完全的一阶逻辑时，我们得到了正确答案的一般定义，它相当复杂，而且远不如预期的一般由于逻辑编程领域的大部分工作都是基于计算的答案，这是正确答案的计算对应物，如果我们想将以前的结果应用于更广泛的逻辑片段，在这里，我们从证明理论的角度来解决正确答案的问题我们认为，“正确答案”的概念自然延伸到一阶逻辑是在一个证明中记录所有出现的量化引入规则。在Horn子句的情况下，如果我们只考虑存在量化器的引入，这是等价的标准的定义。我们还介绍了相应的推广“正确的结果”。然后，我们考虑一个共同的抽象的语义的逻辑程序，即接地，我们研究其扩展的情况下，全一阶逻辑。一个原型的抽象解释这个观察已经开发出来，我们展示了我们已经获得的一些结果。最后，对今后的发展进行了展望。阿马托3S → S S→ S2框架我们在这里给出了一个介绍的微积分，这是一个广泛的推广，大多数的结石已经发展到目前为止，从介绍根岑的LK演算[17]。实际上，我们的形式化是如此的通用，以至于像树演算这样的名称可能更合适。然而，由于我们只在逻辑系统证明的上下文中使用该框架，因此我们将坚持使用微积分的名称。这些主题的更详细的处理可以在[3]和[1]中找到。定义2.1给定一个序列集S，证明框架集Sch（S在S上归纳地定义如下：• 每个S∈ S是一个证明骨架;• 如果S∈ S，n∈N，且Ti是证明骨架，其中i≤n，则T1··· TnS（一）是一个证明骨架，我们也用树（S，T1，.）表示。，Tn）。我们承认n=0的情形。当S从上下文中是清楚的时，我们写Sch代替Sch（S）。然后，我们定义两个函数hyp：Sch（）和root：Sch（），使得• hypp（S）=S，• hypp（tree（S，T1，.，Tn））= hyp（T1）···hyp（Tn），以及• 根（S）=S ，• root（tree（S，T1，.，Tn））= S .给定一个证明框架π，hypp（π）是π的假设序列，而root（π）是π的根。当我们想要声明π是一个证明框架，hypp（π）= S1时，.，Sn和根（π）= S，我们写π：S1，. ，SnS.（二）我们还定义了证明骨架π的高度，引入了函数height：Sch（S）→N，使得• 高度（S）= 0，• height（tree（S，T1，.，Tn））= max{height（T1），.，height（Tn）}+1，其中明显的假设是max（Tn）=0。注意，S（我们也用S表示）和树（S）是两个不同的证明骷髅实际上，它是height（S）= 0和hyp（S）=S，但height（tree（S））= 1和hyp（tree（S））=λ。阿马托4RRS R►∈⊆SRI×···×→现在，我们固定一组高度为1的证明骨架。我们称推理规则为元素。将空的证明骨架和推理规则粘贴在一起得到的证明骨架π称为证明。没有假设的证明被称为最终的。一个S是可证明的，如果有一个最终证明植根于S。最后，我们称微积分为一对（S，R）。2.1语义在下文中，我们假设固定的微积分（S，R）。给定一个证明框架S，我们用SchS表示所有以S为根的证明框架的集合。 对于每个π∈SchS，π：S1，. ，SnS，（3）我们有一个相应的语义算子π：SchS1SchSnSchS ，它通过将输入序列的证明骨架与π粘贴在一起来工作，以获得输出序列S的新证明骨架。 如果Sch是所有的证据π：S1，SnSSch和Xi对于每个i，我们 定义语义运算符π的集合变体，定义为π（X1，. ，Xn）={π（π1，. ，πn）|1≤i≤n。 πi∈Xi<$SchSi}。（4）我们将把π（X）写成π（X，.，X）具有η个相同的拷贝，X作为输入参数。（，）的解释是Sch的子集。我们用所有解释的集合表示，它是子集序下的完备格。一个模型是一个解释I，使得对于每个推理规则r∈R，它是r（I）（五）模型在相同的解释顺序下形成一个完整的格然而，它不是一个子格，因为连接操作符和底部元素是不同的。特别地，模型格的底部元素是我们称之为可编程演算的声明性语义，我们用D表示它。D是（，）的最终证明集。 因此，declarative语义精确地捕获所有终止计算。对于有效处理复合性，我们还需要关于部分计算的信息[6]。如果是所有空证明框架的集合，我们称之为（S，R）的完整声明语义，我们用Dc表示它，最小模型更大然后，可以证明，Dc实际上是所有证明的集合。（S，R）。我们有一个自下而上和自上而下的建设最少的模型使用一对夫妇的运营商，类似的精神，直接后果运营商TP和展开运营商UP的逻辑程序。底部-阿马托5一ααA.A.α≤ I → A◦◦AAupT运算符，将解释映射到解释，定义如下T（I）=I而自顶向下的U运算符是r∈Rr（I），（6）U（I）=以下属性成立：π∈Iπ（R π）。（七）Tω（ω）=D，（8）Tω（ω）= Dc= U ω（ω）。（九）2.2抽象现在可以使用抽象解释的技术[12]来开发一系列用于微积分的抽象语义我们称之为三元组（ ，α，γ），其中（抽象域）是一个有序集w.r.t.关系式和α：（抽象函数）是一个单调函数，γ是右伴随函数。由于（，α，γ）中的α和γ唯一地相互确定[13]，我们通常只通过抽象函数来引用可观测值给定一个观测值和一个关于解释的算子，我们表示为α是上相应的最优抽象算子。我们的框架继承了抽象解释理论的所有共同特别是，以下属性成立：Tω（α（ω））≥α（D），（10）Tω（α（ω））≥α（Dc），（11）Uω（α（ω））≥α（Dc）.（十二）这意味着我们可以计算完全在抽象域A内工作的抽象语义α（D）的近似。根据[10，9]和[2]中介绍的术语，当Tα精确时（即当Tαα = αT）可观测的α被认为是指称的。在这种情况下，等式（10）和（11）中的当Uα是精确的时，可观测量是可操作的，并且等式（12）变成等式。当α既是运算的又是指称的时，它被称为完全的。3正确答案和结果正确答案和计算答案的概念是逻辑程序设计理论和实践的基石。如果我们想将Horn子句的结果扩展到其他逻辑语言，我们需要找到阿马托6Γ→ ∆RR→Bx/a，Γ1，B，C， Γ2→π LΓ→ π1，B，C， π2互换器Γ1，C，B， Γ2→Γ1→ Γ1，C，B， Γ2Γ，B，B→π收缩LΓ→B，B，π收缩RΓ，B→ π Γ→B， πΓ，B→B，π其中B=π或B是原子式Γ→ππRΓ→B，Γ→B→C，γ1Γ→B，Γ→C→B，C →B→C →Γ，B→D，Γ，C→D，Γ，B→C→D，B→LΓ，B1，B2→C，B2Γ→B，B3Γ→C，B4Γ，B1 B2→C，C10Γ→B→C，B→RΓ→B，π Γ，C→πΓ，BC→BLΓ，B→C，Γ→B→C，B→RΓ，B[x/t]→τΓ，τx.B→ ττLΓ，B [x/a] →π[]其中a是新的自由变量Γ→B [x/t]，其中a是新的自由变量Γ→γx.B，γRFig. 1.经典逻辑在新的环境中与这些概念类似。实际上，由于我们不讨论任何计算机制，我们只关注正确的答案。为了清楚起见，我们将假设在一阶经典和直觉主义逻辑的领域中工作。因此，我们有一个项签名，一个谓词签名和两个无限对交的自由变量和约束变量的集合V和W。对自由变量和约束变量使用不同的集合，虽然不是必需的，但极大地简化了定理的证明和陈述[15]。术语和公式的定义与通常一样，序列由两个公式序列组成，由符号→分隔，推理规则是作为图1中模式的实例获得的。当我们想要表示一个特定的推理规则时，我们用实例中出现的公式索引图中模式的名称。例如，<$Lλ，φ，φJ，，是φ，φJ→φ，φ jφφJ→φ，φ.（十三）直觉主义逻辑与经典逻辑的不同之处在于，它允许最多一个公式出现在序列的右侧 常用缩写为x1，. ，xn.φ代表的是100x1。···n.φ。我们还写了φ的存在闭包和泛闭包的φφ和φφ。霍阿马托7恩闭包是形式为Γ→φ的闭包，其中Γ是定义子句的泛闭包序列，φ是定义目标。阿马托8∃∃∀∃∃∀ ∀ ∃∀--∃∀--∃∃3.1作为证明理论性质的正确答案给定一个角S = Γ →x.φ，根据标准定义，一个正确的答案x.程序Γ中的φ是θ的替换，x使得Γ→φθ是可证明的。在下文中，我们将θ称为θS的正确答案。根据这一定义，正确的概念答案似乎与模型理论密切相关。它本质上是x中变量的一个赋值，使得φ在Γ的每个Herbrand模型中都有效然而，如果π是S的一个直觉证明，则通过检查π中的实例，可以从π中提取出πx.φ的正确答案。例3.1如果S是n p（0），x.p（x）→y.p（y），则y/t是每项t的正确答案。如果π是证明IDx.p（x），p（0）→p（0）Rx.p（x），p（0）→该规则给出了正确答案y/0的来源（十四）当我们使用遗传Harrop公式时，我们可以保持与Horn子句相同的正确答案定义。然而，我们通过这种方式获得的信息量相当有限。例如，nx.p（x，x）→ y。z.p（y，z），只有一个平凡的空的正确答案，因为这个公式的右边不是一个存在性的量化公式。对相反，让我们看看同一个问题的证明IDp（a，a）→p（a，a）p（a，a）→<$z.p（a，z）<$R<$x.p（x，x）→<$z.p（a，z）<$RP（x，x）→ P（x，x）z.p（y，z）（十五）如果我们跟踪R和R推理规则的出现，我们得到一个替换y/a，z/a。这使得对于每个y，我们有一个z使得p（y，z）为真，并且y和z重合。此外，如果我们将替换y/a，z/a应用于右侧，丢弃所有在量子数的基础上，我们得到了p（x，x）→p（a，a），这是平凡可证的。如果我们进一步扩展语言来处理完整的一阶逻辑，我们必须处理像x.p（s（x））→y.p（y）这样的序列。 在这里，标准的“模型论”的正确答案定义也没有给我们提供任何有趣的信息，因为根据这个定义，不存阿马托9在正确的答案。实际上，对于任何项t，都不能证明x.p（s（x））→p（t）。让我们阿马托10----∃{∈|π考虑以下证明：IDp（s（a））→p（s（a））p（s（a））→p（y）<$Rx.p（s（x））→（十六）如果我们跟踪一个数量引进规则的所有实例，我们得到一个替换x/a，y/s（a）。 在这里，A的角色是见证人。 左边的存在量化器产生一个新对象a，使得p（s（a））成立。 约束y/s（a）清楚地表明，对象y使得p（y）成立是s（a），其中a是由另一个存在性量化器产生的相同的对象。同样，如果我们应用替换丢弃量化器，我们求出可证明的p（s（a））→p（s（a））。在一般情况下，我们不能用单个项绑定变量。例如，考虑p（a）p（b）→x.p（x），并且证明IDp（a）→p（a）IDp（b）→p（b）p（a）→<$x.p（x）<$Rp（b）→<$x.p（x）<$R（十七）p（a）p（b）→x.p（x）L我们有R模式的两个不同实例，每个实例都有一个不同的项绑定到变量x。因此，我们被引导来考虑类型{x/{a，b}}的绑定。3.2形式化我们现在试图使上述非正式讨论精确化。给定一个一阶语言（T， T，V，W），一个候选答案是函数θ：W→Tf（T（V））使得v W θ（v）=候选答案。是有限的。我们用Ans表示对于每个证明框架π，我们有一个对应的候选答案θπ或回答（π），定义如下：如果π=idΓ，B，θ（x）={a}如果π=πLr，B，x，a（πJ）orπ=<$RΓ，B，<$，x，a（πJ）（十八）如果π=<$R，则为<${t}（πJ）或π=πL（πJ）r，B，x，tj=1. nθπj（x） 如果π = r阿马托11（π1，. ，πn）r，B，x，t如果π是一个证明，那么θπ被称为π的部分正确答案。 如果π是πS的最终证明，那么θ是πS的正确答案。对于CAns（S）的正确答案的集合将由CAns（S）表示，其为阿马托12······∪∀定义为CAns（S）={θπ|π∈ D<$SchS}。（十九）当我们想弄清楚我们是在经典逻辑领域还是直觉逻辑领域工作时，我们写CAnsc（S）或CAnsi（S）例3.2让我们来考虑下S=x。（p（x）<$p（s（x），p（0）→p（y）. 在经典逻辑中，θ是S的正确答案，当且仅当• θ（x）∈θf（Term），• θ（y）∈θ（y），且存在si（0）∈θ（y）使得对任意j∈ {0，.，i-1}。这里si（0）是项s（s（s（0），其中s重复i次。 在直觉逻辑中，正确答案的形式更简单。特别地，θ是S的正确答案当且仅当• θ（x）∈θf（Term），• θ（y）={si（0）}对于某些i ∈ N使得sj（0）∈ θ（x）对于每个j ∈{0，. ，i−1}。这种差异是由于我们不能对后件应用压缩法则。请注意，通常情况下，只有当同一个变量没有两个不同的绑定时，才有意义。在下文中，我们将把满足这个条件的每个元素称为纯元素。我们对正确答案的定义本质上是收集了证明中量化器的所有引入规则的出现问题是，我们得到的大多数答案都是微不足道的。例如，给定一个nx.φ→ n和一个正确答案θ，则θ[x/L]也是一个正确答案，对于每个L=θ（x）T其中T是一组从θ中分离出来的项。因此，我们特别感兴趣的是最小的正确答案，根据明显的逐点排序。对应于最小答案的证明在公式中，我们用 mAnsc（S）（ mAnsi（S））表示问题w.r.t.经典（直觉主义）逻辑例3.3在前面的例子中，经典逻辑和直觉逻辑都有相同的最小正确答案集，即这些θ使得• θ（y）={si（0）}对于某个i∈N，• θ（x）={sj（0）} |j∈ {0，.，i-1}}。请注意，我们有很多信息来自这些。我们知道p（si（0））对每个i∈N都成立。此外，我们知道，为了证明p（si（0）），我们需要对不同项的第一个绑定应用一个新的引入规则，阿马托13/∨ ∃∃联系我们∨∃⊃∃联系我们∃··· ∃也就是所有的sj（0），j从0到i-1。一般来说，如果mAnsc（S）=mAnsi（S），这意味着存在一个关于S的证明，它是“内在”经典的。我们不做精确的陈述，因为它需要进一步的调查。然而，从直观的角度来看，考虑以下证明π的p（a）p（b）→x.p（x）：IDp（a）→p（a），p（b）IDp（b）→p（a），p（b）p（a）p（b）→p（a），p（b）L（二十）p（a）p（b）→x.p（x），x.p（x）<$R2次收缩Rp（a）→p（b）→p（x）如果我们将BRR规则向上移动，在BRL规则之前，我们可以很容易地得到一个直觉证明πJ，使得θπJθπ= x/a，b。然而，考虑以下证明πIDp（a），p（b）→p（b），nRp（a），p（b）→x.p（x），Lp（a），y.p（y）→x.p（x）， Rp（a）→y.p（y），x.p（x）R（2次）p（a）→），）收缩Rp（a）→nx.p（x）n（ny.p（y）n）（二十一）虽然根θ π 是直观可证的，但我们不能写出一个直观证明πJ使得θπJθπ=x/b ，y/b 。这是因为在π中使用收缩法则对于移动的在左侧保持y.p（y），而在右侧保持x.p（x）如果我们将Horn子句的“标准”正确答案与我们的最小正确答案进行比较，我们就有了一个更一般的定义。然而，如果我们把答案限制在存在性数量化器上，我们会得到同样的结果。定理3.4若S= Γ →x1. xn.φ是纯Horn型的，则η是S i的“标准”正确答案，并且存在最小正确答案θ使得θ（xi）= xi η，对于每个i ∈ { 1，... ，n}。请注意，我们没有指定最小正确答案是否应被视为w.r.t.。直觉主义阿马托14或经典逻辑。实际上，如果S是一个纯Horn矩阵，它是mAnsi（S）=mAnsc（S）。阿马托15∈[2014-05-23]3.3生成物SLD-导子的另一个典型抽象是结式的抽象[16]。程序P中目标G的结果是由G的部分计算答案和仍需要反驳的新目标G我们提出了一个可观察的证据骨架，这是灵感来自这个到目前为止，我们一直认为序列是公式的序列然而，经典逻辑和直觉主义逻辑通常通过将一个函数定义为一组公式来表示。我们使用术语集合S来表示这个替代定义，我们用集合S表示所有集合序列的集合。如果S∈S，我们将Set S中的相应元素记为S′。我们称结式为对（θ，S），其中θ而S是一个有限的多重集合，设置序列。我们用Res表示所有结式的集合。对于每个证明骨架π：S1，. ，Sn<$S，我们定义一个相应的res（π）为res（π）=（θπ，[S<$1， . . ，Sn），（22）哪里表示多集合。 如果π是一个证明，那么res（π）是S的正确结果。S的正确结式集将由CRes（S）表示，其定义为：CRes（S）={res（π）|π∈Dc<$SchS}。（二十三）当我们想指定我们是否在工作时，我们写CResc（S）或CResi（S）在古典逻辑或直觉逻辑的领域。我们根据以下等式（θ，S）≤（θJ，SJ）i <$θ≤θJ且S <$SJ.（二十四）再次，我们谈论的最小正确的结式的元素CRes（S）是最小的w.r.t.≤。我们将相应的集合表示为mResc（S）和mResi（S）。例3.5让我们考虑下式：S=p（0）→x.p（x）。 集合mResc（S）包含所有对（θ，S），使得• θ={x/0}和S=θ，或• θ={x/t}，其中t= 0且S=[p（0）→p（t）]，或• θ ={x/t}，其中t= 0且S =[p（0）→x/t]。对于mResi（S）也是如此。证明正确的答案和正确的结果之间存在下列对应关系是很容易的：CAns（S）={θ|（θ，θ）∈CRes（S）}，（25）mAns（S）={θ|（θ，θ）∈mRes（S）}.（二十六）阿马托16→S → S →4可观测量既然我们已经定义了什么是正确的答案，我们想为CAN和MANS找到一个自底向上和自顶向下的构造。遵循[3]中的抽象框架，我们将候选答案的可观察性定义为元组[（Ans）]，αc，γc，其中[是从序列到候选答案集合的函数集合，αc（I）（S）={θπ|π：·εS∈ I}。（二十七）证明αc（D）（S）恰好是所有正确答案的集合CAns（S）是很简单的。对应于T的最优抽象算子为Tαc。假设A在αc的像中，则为Tαc（A）（S）= A（S）<${rαc（A）|r ∈ R，root（r）= S}，（28）其中，对于每个r：S1. Sn<$S∈ R，rαc（A）={rαc（θ1，.，θn）|i∈ {1，.，n}，θi∈A（Si）}，（29）和<$θ1<$<$[x/t]如果r是一个量化器的引入规则rαc（θ1，. ，θn）=它将绑定变量x替换为t，否则θ1· ··θn。（三十）在这里，我们将候选答案θ写成θ1<$θ2，使得对于每个x∈V，θ（x）=θ1（x）<$θ2（x），并将候选答案θ写成[x/t]，使得θ（x）={t}，θ（y）=<$，对于y/=x。定理4.1候选答案的可观测值αc是指称的。我们也有一个可观察的结果，它给出了起源，以完成自底向上和自顶向下的语义。 它被定义为元组→[集合S] →用抽象函数表示的[R（Res）]，αr，γrαr（I）（S<$）={re s（π）|π∈I，r oo t（π）=S<$}。（三十一）最佳自底向上定点算子的定义是直截了当的。关于自顶向下定点算阿马托17子，假设A在αr的像中，我们有Uαc（A）（S<$）=δ（R），（32）δ∈A（S<$）阿马托18联系我们∈其中，如果δ=（θ，[S<$1， . . ，S<$n），δ（X）={δ（[π1， . . ，πn）|i∈{1.. . n}，πi∈X<$SchSJ且S<$J=S<$i}，我我（三十三）和.Σδ（[π1，. ，πn）=θ<$[x1/t1]<$··<$[xm/tm]，[hyp（π1），···，hyp（πn）<$、（三十四）其中，对于每一对（xi，ti），有一个量化器的引入规则，{π1，.，πn}，其用t i替换变量xi。定理4.2正确结式的可观测αr是完备的。由于αr是一个完美的可观测量，我们可以建立一个自顶向下的解释器来计算正确的结果。然而，这种解释器的有效实现是一个非常困难的任务，这是自动演绎的领域。在这里，我们更感兴趣的是计算正确的结果的抽象，它可以用于逻辑语言的静态分析4.1接地如果θ是S的一个候选答案，当θ（x）只包含在S中自由出现的变量时，我们说θ是变量x的基础。让我们用GAns定义函数集V（g，ng），我们称之为基性答案。给定一个候选答案θ，我们定义一个相应的基性答案β=基S（θ），使得• g∈β（x）i <$存在t∈θ（x）使得vars（θ）<$FV（S），• ng∈β（x）i ≠存在t∈θ（x）使得vars（θ）/<$FV（S），其中FV（S）是S中自由变量的集合。然后，我们可以定义一个伽罗瓦连接→αg，[S→（Ans）]，[S→（GAns）]，γg，其中αg（A）（S）={groundS（θ）|θ∈ A（S）}。（35）然后，将αg与αc相结合，我们得到一个观测值→ε（GAn s），αg<$αc，γc<$γg为接地答案。如果β∈αg（CAns（S）），则β是正确的有理数答案。此外，如果β αg（mAns（S）），则根据明显的逐点排序，β是最小的阿马托19例4.3让我们给出一些数列及其对应的例子阿马托20我我我直觉逻辑的正确最小根据答案。sequenty.p（y）→很好（p（a，y）<$p（y，b））→<$x.p（x，x）p（a）<$r（b）→<$x。（p（x））n→nx.p（x）p（y，y）→x1. x2.p（x1，x2）1. 2. p（x1，x2）→ny.p（y，y）y.p（y）→p（t（a））→nx.p（r（x））p（a）n =x.r（x）n =y. （p（y）r（y））接地答案{x/g，y/g}{x/ng，y/ng}{x/g，y/g}{x/g}{}{y/g，x1/g，x2/g}，{y/ng，x1/ng，x2/ng}-{x/ng，y/ng}-{x/ng，y/{g，ng}}请注意，如果θ是S的正确答案，x是一个只出现在负存在quantier中的约束变量，那么θ不是X. 正通用绑定也是如此。我们可能会问自己，我们的可观察域和标准域之间的对应关系是什么，以分析POS[5]。有可能证明下列情况定理4.4设P是一个确定规划，G是一个确定目标。我们在直觉逻辑领域工作假设S = r →rx1，.，xn. G是相应的纯Horn数。 考虑x1，. ，xn作为命题符号并定义公式Θ ={θi×β（ xi）}，（36）β∈GAns（S）其中x{g}= xi且x{ng}=<$xi。 则Θ是正公式。此外，如果X是G在P中的正确答案集，则令α = αPOS（X）。则θ和Θ是等价的公式。我们也可以从结果开始建立一个基础分析的抽象。给定一个公式φ，我们用αv（φ）表示一个抽象公式，这个公式是通过把每一项替换为其中出现的自由变量的集合而从φ得到的。我们称从抽象公式得到的抽象集合序列的 一个基性结式是一个对（β，ν），使得β∈GAns，ν是GS的元素