基于分层地图推理的实验方法

理论计算机科学电子笔记48（2001）网址： http://www.elsevier.nl/locate/entcs/volume48.htmlpp. 1- 28分层地图推理：在第1组上进行试验的实验方法Andrea Formisano2佩鲁贾大学数学和信息学系尤金尼奥湾Omodeo3Dipartimento di Matematica Pura edAppliata，Universit`adiLMarco Temperini4罗马大学信息与系统学院摘要新的成功，在处理集理论的国家的最先进的定理证明，可以随之而来的简洁和简洁的公理系统，如可以塑造的框架（完全等式）塔斯基-吉万特形式主义的二元关系，这里命名为“地图”。本文为基于这种公理系统的系统实验奠定了基础。 在映射代数的核心公理化之上，我们开发了基本集合论概念的分层形式化。 在一阶定理证明器的协助下，本文报道了在这个框架内进行的一些具体实验。其目的是评估所提出的分层架构的潜在有用性，并在一定程度上揭示了有前途的，以最好地调整它。关键词：集合论，关系代数，一阶定理证明，代数逻辑。1这项研究得到了意大利IASI-CNR（协调项目）的部分资助log（SETA））和MURST（PGR-2000-Automazione del ragionamento in teorie insie-mistiche）。2电子邮件：formis@dipmat.unipg.it3电子邮件地址：omodeo@univaq.it4电子邮件：marte@dis.uniroma1.it2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。福尔米萨诺、奥莫代奥和泰姆佩里尼2L1介绍鉴于它在精确科学中的普遍性，集合论值得持续的研究，以揭示它的越来越丰富的可判定片段[7]，用于推理的一般推理规则[36，2]，基于其领域知识的有效证明策略[3]，等等。虽然自动推理的这个专门领域取得了进展，并取得了自主的结果和更大的视野（参见。[9])许多集合论的实验都是通过标准的定理证明系统进行的。直到今天，这样的实验仍然对最先进的定理证明器造成了相当大的压力，或者要求用户对证明助手给予很多指导;因此，它们构成了理想的基准。即使对于那些努力在集合论这个充满挑战的领域中开发一些完全特设的东西的人来说，重要的是要评估今天通过非专业化的证明方法可以实现什么，以及集合论的特定于上下文的瓶颈确切地存在于哪里。在其最流行的一阶版本，即Zermelo-Skolem-Fraenkel公理系统ZF中，集合论（非常像皮亚诺算术）提出了一个直接的障碍：它不承认有限公理化。这就是为什么Neumann-Bern的集合和类的Güodel理论有时更倾向于作为实验的基础[5，35，30]。不同的作者（例如，[24，28，29]）已经能够保留ZF的特征，通过诉诸特定定理证明者的高阶特征，如Isabelle。在这篇论文中-继续[17]开始的系列-我们追求一种最简方法，依赖于ZF和有限集理论（首先在[33]中提出）的这些公式是基于逻辑系统L×深入研究，[34]我们设计它们的目的是为实验提供一个好的起点--比如说，用Otter[23]，或者用一个更明显的等式定理证明器。我们的公理化任务的指导方针也来自[34]：结果是等式的，没有变量，因此一些-什么不符合标准。幸运的是，用×表示的理论可以很容易地通过一阶系统来模拟，只需处理它的公理（包括逻辑公理和具有真正集合论内容的公理）的图解公式，在实践中，这意味着将ZF视为关系代数理论的扩展[20，22，12，32，26，14，18]，其变量不应该在集合上，而是在并矢上（即，二进制）关系的集合的宇宙。无论如何，我们自己的ZF公式一方面与ZF本身的确切关系，另一方面与GB的确切关系，是一个微妙的理论问题，我们打算在本系列的另一篇文章中加以解决本文共分两部分：• 第2-[15]，[17，Sec.7.2]-我们的集合论公理的等式公式在其福尔米萨诺、奥莫代奥和泰姆佩里尼3L∈ ULUL−1∈U U × ULU整体，集合论o提出了一个全景的替代品（参见。[31，p.x]）;也就是说，它由公理系统不等价（有时是对立的，参见。[25])彼此之间。这就是为什么，我们不是只给出一个理论的公理，而是指出各种选择。未来的工作将扩大这些部分的材料到一个工具包组装类和集合理论的所有种类后，我们已经挑选出来，通过实验，公式的公理，工作肯定比别人更好。• 第4-与基于更传统的集合公理规范的类似结果的比较，将推迟到本系列的另一篇论文中，这些结果充分利用了一阶谓词语言的表达手段。2L×的公理、语义和逻辑公理×是一种基本的等式语言，人们可以在一个未指定但固定的话语域上陈述二元关系的性质--我们称之为MApS。我们打算指定其性质的映射是所有集合类上的隶属关系语言×由映射等式Q=R，其中Q和R是映射表达式：定义1MA pEXPRESSION是顶部所图1-其符号，，Δ，，\，，†将被用作左结合在fix运算符中，作为一个后期修复操作员， 作为其论点的一条线。✷对于×的解释，必须固定一个子集，以及一个非空的子集«关于2=默认值然后，每个映射表达式P来设计一个特定的映射P«（因此，映射之间的任何等式Q=R表达式结果为真或假），基于以下评估规则：nn=Defn，ln=DefU2，ln=Def{[a，a] ：U中的a};（Q<$R）<$=Def{[a，b]∈Q<$：[a，b]∈R<$};（QΔR）<$=Def{[a，b]∈U2：[a，b]∈Q<$当且仅当[a，b]∈/R<$};（Q<$R）~（n）=Def{[a，b]∈U ~2：对于U中的某个c，有[a，c]∈Q~（n）且[c，b]∈R~（n）};（Q−1）<<=Def {[b，a]：[a，b] ∈ Q<<}。在×的签名中的运算符和常量中，只有少数几个值得被视为原始构造;实际上，我们选择将我们没有给出求值规则的那些构造以及其他构造视为派生构造我们将默认添加到签名-见图的中心部分。1.一、福尔米萨诺、奥莫代奥和泰姆佩里尼4UUC►LLCL×的解释显然延伸到新的构造;例如，（P<$Q）<<=Def{[a，b]∈ U2：对于U中的所有c，[a，c]∈P<或[c，b]∈Q<<}，funcPart（P）=Def{[a，b]∈P：[a，c]∈/Pforanyc/=b}，因此funcPart（P）=P将意味着请注意，我们还允许自己通过简化定义来定义遵循某些模式的映射等式的替代符号。这是，例如，符号Func（P）的情况，其含义与funcPart（P）=P相同;或者Total（P）的情况，其声明对于所有a，在P</$∈）<$/∈））<$/$当b和x/∈<。共轭准投影{{b}\{a}，{b}\{a}}是哪里λDefν−1和ρDefvalve−1（∈∈，ν），v<$Def/∈∈ <$valve（∈∈，/∈∈）.正如我们将在后面讨论的，（Pair）可以从（E）、（N）和（WL）导出。一个无穷公理和替换公理我们在图2中收集了迄今为止介绍的所有公理，以及（Pair）的附加子句，经典替换公理的一个版本（Repl），以及公理（I），该公理（I）以（R）为前提，说明无限集合的存在（参见。[27]）。当然，这个无穷公理与前面看到的公理（F）是对立的：人们可以采用其中任何一个，但只能采用两者中的一个。新公理（Pair）5、（Repl）和（I）在这里不讨论：感兴趣的读者可以在[15]中找到详细的评论。4在Otter为了遵循[34]的正统性，我们应该把×当作一种自治的形式主义，与一阶谓词演算等同然而，这会给我们带来两个问题：我们应该从头开始为×建立一个定理证明器，我们应该处理（S）和（Repl）的无限多的例子。幸运的是，如果我们把出现在逻辑公理或（S）、（Repl）中的元变量（以及在归纳方案中，如果任何元变量作为附加公理或待证明的命题而发挥作用的话）视为一阶变量，则这是不必要的。在一阶逻辑的框架内，逻辑公理失去了它们的地位，成为关系代数上的公理，在概念上形成了公理集合论的一章，它本身就很有趣，比布尔代数更丰富，比公理系统的其他部分更基本和稳定。福尔米萨诺、奥莫代奥和泰姆佩里尼10.Σ.Σ其中， n（P）≠Def P○/∈，F（P）Def （P）\P○∈图二.映射演算任何标准的定理证明者，例如水獭，可以利用实验公理一样，关系代数（cf。图1）和我们到目前为止已经检查过的集合上的那些（浓缩在图中）。2）的情况。Otter（Organized Techniques for Theorem-proving and EECHIFICATIONResearch）是一个由Argonne National Laboratory开发的解析式定理证明器（参见[23]了解详细描述）。它可以操纵以完全一阶逻辑写的语句Otter中可用的推理规则有：二进制解析、（有序）超解析、UR-解析和二进制调制。Otter• 输入可以是合取范式，或完全一阶逻辑;• 前向解调用一组等式重写和简化任何新推断的子句，后向解调使用新推断的等式重写所有现有子句;• 前向包含删除被任何现有子句包含的推断子句，后向包含删除被推断子句包含的所有子句• Knuth-Benchmark方法的一个变体可以搜索一组完整的约简;• 权重函数和词汇排序决定了分句和术语的（E）F（$）=i（N）Total（1l∈）.Σ（WL）/∈ ∈（∈∈\i○（∈ ∈/∈∈））○$=1l（Pow）总计（（/$∈））（单位）共计（美元）（T）合计（e ○（i））（$$）.Σ（S）总F（func Part（Q）○$FUP）（Pair）1，2，3，4λ−1○ρ=1l， Func（λ），Func（ρ），∈$=1l（对）5λ○λ−1<$ρ ○ρ−1\i=<$（F）<$$>1l○ ∈ <$（（<$$>/$∈）<$/$（R）1l∈=1l○（∈\$∈）.Σ（I） T总1l○（（$$）（$$）−1\ ∈ \$ \i\ $ ○∈ Δ $ ○ ∈）（Repl）总函数（（λ○$○λ1<$ρ○ρ1）○funcPart（Q））福尔米萨诺、奥莫代奥和泰姆佩里尼11• 采用一组支持策略Otter提供了大量的参数和选项来帮助用户指导推理过程。下面我们简要说明我们在实验中发现的更有用的方法。这将通过给读者描述的基本策略，我们通过证明定理与水獭。正如我们将看到的，在大多数情况下，这种策略工作得很好，而我们需要某种调整才能成功地处理一些定理。因为我们处理的是等式，所以我们选择了Knuth-Benzinger完成过程;每当非单位子句或非等式谓词开始起作用时，我们就启用超归结和二元归结。采用了参数调节。我们通常利用缺省策略进行排序、分句解调和加权。另一方面，我们系统地使用了用于限制搜索空间的参数。为了更详细地说明，所有的定理都是在一个派生子句中文字的最大数量和派生子句中不同变量的最大数量上此外，我们经常对派生子句的权重设置一个阈值：比这个值“重”的子句我们还采用了Otter的默认加权策略（参见[23]);在某些情况下，我们发现给某些项或文字额外的权重以减少寻找证明所花费的时间是有用的。这里是我们在证明几乎所有的映射演算定理时使用的Otter设置（对于这里没有提到的参数和标记，我们保留了Otter的自治值）。模式）：%策略：set（knuth bennett）.set（backdemod）.设（段）。set（hyper res）.set（parainto）.set（binaryres）. set（dynamic demod all）.搜索空间%限制：assign（max distinctvars，3）.assign（max，1）.assign（max weight，18）.请注意，分配给最大权重的值通常是在地图推理与水獭的初步实验已在[1，17]中描述;在[15]中，提出了一个集合理论的方程再造在[10，16]中探讨了基于ZF集理论的这个方程式表述的自动集推理。特别是，在[10]中，作者获得了一个基本结果的（半）自动证明：在非常弱的集合公理下，即（E），（N）和（WL），有可能导出一个对的存在性福尔米萨诺、奥莫代奥和泰姆佩里尼12的投影满足配对公理（cf.秒5、看得这一结果，将在第二次世界大战期间进行简要调查。5，保证了ZF的方程式与其一阶版本的证明方法的等价性（参见。[34]）。[10]中报告的实验活动完全依赖于Otter提供的自主模式，并且始终采用默认设置。避免了参数和标记的显式调整，以使该方法与特定的定理证明器具有更高的独立性由于[10]中处理的定理的语法复杂性相当低，这种方法代表了一种可行的选择。我们在这里要描述的活动旨在证明涉及集合理论概念的定理，这些概念的语法和语义复杂性随着实验的进行而不断增长这个事实可以很容易地通过考虑概念的更高层次的抽象来理解，例如总体性或功能性。基本的地图结构。为了反映这种复杂性的增长，我们将开发一个分层的引理层次结构从一个由图1的结构和公理组成的“内核”开始1，我们将通过定义新的集合论概念和证明表征新的集合构造的定律组来系统地进行这些扩展步骤中的每一个都将是下一个扩展的基础（潜在）的一部分。此外，在证明一般定理时，可以选择可用构造的子集及其定律。实际上，这将有助于以两种正交的方式搜索证明：首先，Otter将只处理用户判断为与要证明的定理相关的全局环境的一部分;其次，推理活动将更好地集中在最合适的抽象层次上。例如，在证明一个定律时，这个定律从组成部分的总体中推断出地图的组成的总体（参见图1）。图11），不需要深入处理开发我们的层的第一步是证明一系列用于内核构造的辅助算法（namely，Δ，，○，−1）。 从理论上看，这些定律是没有必要证明任何（可证明的）映射演算定理然而，实验表明，奥特无法在合理的时间内证明几个简单的定理，除非使用这些辅助定律。法律的显著部分关于Δ和Δ的关系，如图所示3、地图构图的规律（C1组）和地图反演（G1组）。四、定律被分成几组，因为每组通常对应于一个可以加载到Otter中的输入文件;此外，同一组中的定律通常通过采用相似的参数设置和搜索控制来证明，并且通常使用相同的前提组作为假设。对于表中的每一条定律，我们指出：a) 作为输入给Otter的公式组b) 水獭发现的证据的长度福尔米萨诺、奥莫代奥和泰姆佩里尼13法处所len. 时间将军保持I1 P\=Ax2071120185P\P=PAx20132304382P\（P\Q）=P\QAx27132157318I2 P\Q=P→Q=P轴，I11<1224P\Q=Q→P\R=P轴，I12316262S1 P4Q=Q 4PAx7219552P4（Q4R）=Q4（P4R）Ax8425854104P=PAx2081124190P4P=Ax1651110180P4（P4Q）=QAx5223452\（P4P−1）=轴，S1199 5分 30秒六、4·10613842P\（Q4R）=（P\Q）4（P\R）轴，I1，S 12212045图3.第三章。关于Δ和Δ的定律法处所len. 时间将军保持G1 −1=Ax22814342261l−1= 1lAx4<18540−1=Ax3<13822（P41l）−1=P−141l轴，S143 1 .一、33S24972 2033（P4Q）−1=P−14Q−1轴，S1，G189 1 .一、12s17147 1554C1 ØP=0Ax2691447231P =Ax1781378219P=PAx4238231l 1l= 1lAx29203215526（（PP−1）\）P=P轴，G1，C166十八岁53s221080 8774P（（PP−1）\）=P轴，G1，C171十九岁02秒227467 8844P\（P11）=PAx62六、36S68558 6734P\（1lP）=PAx61六、08s67926 6646图四、关于-1和0的定律c) 花费的时间（如果没有不同的规定，则以百分之一秒表示）;d) 在推理过程中生成的子句的数量：e) 保持的子句的数量（即，生成的子句满足对权重、变量数量、文字数量等的所有限制在我们的实验中，我们在PC（Pentium III-450，128 MB RAM）上使用了运行在Linux下的Otter 3.0.6。注意，有时候保留的子句比生成的子句多这是因为前者包括通过处理输福尔米萨诺、奥莫代奥和泰姆佩里尼14入公式集获得的所有子句大多数定律的写作福尔米萨诺、奥莫代奥和泰姆佩里尼15法处所len.时间发生器保持N1P =P=1l1l=P\Q=Q4（P\Q）P4Q=P 4Q P4P=1lP\P=0N2P−1=P−1P4P=1lP\Q=P→P\Q=PP\Q=P→P\Q=P\P−1P=P4Q=P\Q\P\QP4Q=P\Q\P\QP4Q=P\Q\P\QP−1\Q−1=（Q\P）−1Ax轴轴Ax、 N1、 S1、 I1、G1JJJJJJJJAx，N1，S1，I1，G1，N2. 6JJJJ7 105 41645 385560 182（P4Q）−1=P\Q\P\Q−1320435219553219122931817912153081143617792257572<14024181522104961204012040431646884181712017233646718375012143542 10米36秒1。2·107 13860图五.地图互补证明;否则，输入中只给出了关于定理中出现的构造的（部分）公理例如，为了证明法律(1)（（P○P−1）i）○P=P对于群C1，我们利用了G1和C1的定律（这意味着Otter可以在C1中使用前面（1）列出的定律）;此外，我们还加载了Ax相对于○和−1的部分。图5和图6分别列出了地图互补和地图合并的法则。这些结构的定义在原始的定义中列出图。1，连同其他概念的地图形式化，将在续集中发挥作用。图8中列出了关于地图组成和i的表达性质的其他定律为了证明这些定律，水獭需要使用互补和联合的定义图构造，以及它们的定律。值得注意的是，如果不使用I1、C1、G1、U1、2、3、4中的定律，Otter无法在合理的时间内证明图8中的几个定律。接下来是关于映射包含和左绝对性的定律。签名的这种扩展可以被视为对地图的整体性和功能性进行研究的准备。反过来，关于总体性和功能性的定律将在证明我们将在后面的章节中报告的集合论命题中发挥关键作用。关于Otter面对地图演算的行为，有几点评论。首先，实验表明，一般来说，证明定理/定律福尔米萨诺、奥莫代奥和泰姆佩里尼16法处所len. 时间将军保持U1 P[Q]=Q[PAx8<110746P=PAx1936751221l[P= 1lAx6321065P[P=PAx24131746478（P\Q）[（P\R）=P\（Q[R）Ax27181939597（P\R）[（Q\R）=（P[Q）\RAx423846691046P\（P[Q]）=PAx32171920567P\（Q\（P[R））=P\QAx37171951604P[（P\Q）=PAx33161916559P[（P\Q）=P[QAx39161986648P[（P\Q）=P[QAx36171981622（P\Q）[（P\Q）=QAx35181996624P [P=1l轴，N192028P[Q]=P\QAx19111298448P\Q=P[QAx18121275435U2 P[（P[Q）=P[Q轴，U16210168（P[Q][R]=P[（Q[R]）轴，I1，C1，U16二、74秒69861 1047P[（Q[R）=Q[（P[R）JJ4二、62s68421 1035（P[Q]\（P[R）=P[（Q\R）JJ131 .一、41s39504709（P[R]）\（Q[R]）=（P\Q）[RJJ301 .一、4439550729P[（Q[（P\R））=P[QJJ371 .一、4839872735（P[Q）[（P\R）=P[（Q[R）JJ11112232300U3 P[Q=0→P= 0P4Q=（P\Q）[（P\Q）轴，U2JJ28241 .一、84秒23326090682116（P[Q）\（P\Q）=（P\Q）[（P\Q）JJ53377033792P4Q=（P[Q）\（P\Q）JJ431 .一、44S25517 1802\（（P\P−1）[（P\P−1））=JJ359 .第九条。60年代101784 9462\（（P\P−1）[（P\P−1））=轴，U2，U365094U4 （P[Q]R=（PR）[（QR）Ax92288144（P（Q[R））−1=（（PQ）[（PR））−1轴，G1424259591508P（Q[R）=（PQ）[（PR）轴，U424377141图六、地图联合法则福尔米萨诺、奥莫代奥和泰姆佩里尼17法处所len. 时间将军 保持Y1 PQ\R=→P−1R\Q=Ax56132104 328T1 P =0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000埃克斯河13226252 362P1l= 1l 1lP= 1l埃克斯河2224062图7.第一次会议。循环定律和简单性的某些结果似乎更具挑战性（与我们的推理机制）时，地图或者它的某些属性。例如，考虑图3中的倒数第二定律，以及涉及C1或C2中的i的定律。对于那些对应于i的深层内在特征的定律，也可以这么说，例如福尔米萨诺、奥莫代奥和泰姆佩里尼18法处所len.时间将军保持C2 P\（P（Q\））=P（Q\）P\（（Q\）P）=（Q\）P P\=P−1\（P\）−1=P−1\（P\）−1=P\Ax，I1，C 1，G 1，Ui，Y 1JJJJJJJJ21217637420. 61秒四十52秒四十34S743号。47突击步枪23637058445756899394661687813644150521488516015167P−1P\=（P−1（（PQ）41l））\Q=（P−1（R\（1l4（PQ）\Q=（P-1P） Q）\Q=（P−1（R\PQ））\Q=Ax，I1，C 1， 2，G1，Ui，Y 1轴轴Ax、I1、C 1、 3、G1、Y 1Ax、I1、C 1、 3、G1、Y 11353424四、78秒9152959433121724722042335670724144246192C3CJ3图8.第八条。更多关于地图构图和属性：（2）对于每一个Pi，P−1= P成立。这种现象可以直观地解释为，观察到诸如（2）断言的属性不涉及作为单个对象的映射，而是断言属于映射的每对组件之间的关系。从某种意义上说，这类陈述可以被认为具有“更深层次的特征”，或者换句话说，是对话语领域的一种深层知识的其次，简单的句法变化（保留语义）在-sis被证明有时严重影响水獭例如，考虑法律(3)PΔQ=P<$Q<$P<$Q图五、它的证明对水獭来说相对容易，如果与(4)PΔQ=P<$Q<$P<$Q它可以从（3）通过应用规则获得P=Q× P=Q并利用双重否定定律P=P。为了找到这种“不稳定”行为的可能的合理性，我们必须考虑Otter采用默认的术语词典排序（每当用户不提供自己的标准时），以便定向重写规则（回忆Knuth-Benzen完成被采用），并处理解调和加权。在上面提到的情况下，两个主题的默认顺序是相同的，但前者的效果更好。改变字典排序的标准（在证明（4）中）将确定更好的性能。作为对这一现象的最后一点评论，请注意，正如人们所期望的那样，福尔米萨诺、奥莫代奥和泰姆佩里尼19（4）的证明是非常容易的（参见。图（5）当（3）福尔米萨诺、奥莫代奥和泰姆佩里尼20法处所len. 时间将军保持Inc1 PPAx、I1、C 1、G1、N 1、U 1JJJJJJAx，I1，C1，G1，N1，U1，4，Y1，Inc1Ax，I1，C1，G1，N1，U1， 4，Y 1，Inc 1， 2JJJJJJ134658PQ→（QR→PR）84362107PQ→P−1Q−1771582229PQ→（RS→（P\RQ\S））1674193771638PQ→P\Q=P12050ØP133250Inc2 PQ→（RS→（PRQS））161分 16秒2·1063425Inc3 P\Q=P→PQ13154PQ→（QP→P=Q）3320565\PP4541390\PP−1242分 30秒3 .第三章。3·10625386PQ→QP981641268PQ→（RS→（P\SQ\R））10 十一岁46S76721289711lPP−1=1JJ193781991002P1lJJ23210651l 1lP= 1lPJJ36 10个。23S1667788485PQ→（PR→（PQ\R））PQ→PP−1QQ−1JJJJ221525338160677301586Ax，I1，C 1，G 1，Inc4 1lP\P=0N1、U 1、 4、Y 12587188611713P1lPAx，I1， 2，C1， 2，3'，G 1，N1， 2，Ui，Y 114201104PP1lJJ1616499P\Q（1lP）\QAx，Inc1， 2， 335818235P（（11Q）\R）=（11Q）\（PR）Ax，lAbs1. 1077 1 .一、57S174422695Inc5 （P\Q）RPR\QRAx，Inc1， 2， 36185199281P（Q\R）PQ\PRAx，Inc1， 2， 36185199281图9.第九条。地图收录法在假说中。也有一些法律的情况下，其证明变得更容易，如果一些额外的引理在输入（参见，例如U3或1Abs1）。这是我们选择将关于特定地图构造的定律分成几组的动机水獭表现出不同的行为，甚至在证明同一个论点时，制定在不同层次的