定理的差异：逻辑学家与数学家对定理的概念和应用的差异的研究与建立自动发现系统的初步结果

理论计算机科学电子札记151（2006）21-38www.elsevier.com/locate/entcs数学定理1Roy L.麦卡斯兰，2，艾伦·邦迪a，3 和帕特里克·F. 史密斯B，4a爱丁堡大学信息学院英国苏格兰爱丁堡英国苏格兰格拉斯哥大学数学系摘要对于大多数逻辑学家来说，“定理”这个词指的是任何被证明为真的陈述，而对于数学家来说，“定理”这个词相对来说很少被应用，并且表示更特殊的东西。在本文中，我们研究了术语差异背后的一些根本原因，并展示了如何利用这种差异，以建立一种计算机系统，它能自动地从前者中选择后者类型的“定理”。事实上，我们已经开始构建自动发现系统MATHsAiD，其设计基于我们的研究。我们提供了这个系统产生的一些初步结果，并比较这些结果出现在各种数学教科书中的定理。保留字： 自动定理生成，数学推理1介绍对大多数逻辑学家来说，“定理”这个词1作者得到EPSRC MathFIT基金GR/S31099的支持2Email：rm cc asla@inf. ed. 梭uk3Email：A. Bundy@ed. 梭uk4Email：pfs@maths。gla。梭uk[5]在本书中，1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.02122R.L. McCasland等人/理论计算机科学电子笔记151（2006）21相对而言，很少使用，并且表示更特殊的东西。在本文中，我们将研究一些背后的差异术语的根本原因，我们展示了如何利用这种差异，以建立一个计算机系统，自动选择的“定理”之间的这一区别的重要性不应被低估，因为数学家的这种能力似乎可以合理地预期，如果机器学习或人工智能系统能够至少在某种程度上模仿这种能力，那么这个系统也可能能够继续“发现”新的定理，避免通常的规模扩大困难特别地，这种系统在某些应用（例如，形式方法），目前，很难派遣所有出现的证明义务，而不首先发现和证明一些必要的（或至少是有用的）引理。在任何情况下，如果找不到某种方法来识别那些在某种意义上是新的真理，任何这样的系统的替代方案将是要么存储每一个新发现的事实上，我们已经开始建立一个计算机系统，称为MATH-sAiD（从H形数、Axi oms和D定义中机械地确定T 虽然这项工作仍处于相对早期的阶段，但结果是相当有希望的。读者应该明白，虽然，这篇文章并不打算提供一个系统的描述相反，目前，我们专注于系统的定理过滤部分背后的原理和哲学。然而，我们在附录中包括了MATHsAiD选择作为定理的状态样本也许应该指出的是，我们的研究受益于这样一个事实，即两位作者已经6粗略地说，每当MATHsAiD被赋予一组公理（定义）进行研究时，它就会建立一系列假设集，对于每组假设，依次，它使用前向链接过程来生成从这些假设得出的定理这个顺序是由每个公理的性质决定的也就是说，公理被划分为类（例如，关系、操作、关闭类型等），每个类都以这样一种方式对待，以便（希望至少）使MATHsAiD能够找到人们可能会寻找的更常规的结果，关于所说的类。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2123在数学研究方面有相当丰富的经验，另一位作者，谁是训练有素的逻辑学家，有相当丰富的经验，在人工智能的研究。还应该指出，我们的想法在很大程度上受到了[4]和[6]中所作工作的影响。作者知道其他人已经做了一些相关的工作（参见，例如，[2]，[3]，[5]，[7]和[11]）。然而，据我们所知，没有其他人采取我们的办法来解决这个问题，也没有任何人取得完全令人满意的结果。2一些替代方法在继续之前，我们简要地提到一些我们和其他人已经考虑过的替代方法。人们可以尝试应用各种不同的技巧，其中最流行的似乎是“有趣”。然而，我们认为，试图量化“兴趣”既不实际也没有用，因为这个概念，至少当它被应用于数学定理时，是完全相对的。[8]在这方面，不仅各个数学家之间会有一些分歧，而且今天某个数学家感兴趣的东西，一年后他（或她）也不一定感兴趣。无论如何，教科书中记载的大多数定理，在数学家看来，在“有趣性”这一类别中，得分可能都不太高。然而，数学家们通常会同意，同样的定理被适当地贴上这样的标签。或者，可以尝试衡量“重要性”或“有用性”。例如，我们可以计算一个给定的定理在证明连续定理时被使用的次数，然后只选择那些计数超过某个阈值的真理作为定理。人们甚至可以进一步扩展这一点，给每个相继的定理附加权重，并相应地调整给定定理的计数。乍一看，这种方法似乎有点希望。然而，许多工具，数学家发现最有用的在他们的研究中，不会，事实上，被他们认为是定理。此外，结果将在很大程度上取决于所使用的定理证明器的特性，以及材料的顺序。本文介绍因此，我们预计这种做法的结果不会令人满意。[7]见前一节末尾的参考资料。[8]事实上，关于什么才是数学定理的确切构成的整个概念在某种程度上是相对的。事实上，我们并没有衡量成果的“黄金标准”。也就是说，通过将我们的结果与数学教科书（见第4节）进行比较，我们可以对我们的研究是否至少取得了一些成功有所了解24R.L. McCasland等人/理论计算机科学电子笔记151（2006）21事实上，从我们的角度来看，这种方法的主要缺点事实上，这是我们的系统与前面提到的其他系统之间的主要区别。3数学和逻辑我们的基本哲学，关于MATHsAiD，是系统中使用的所有方法，在某种意义上，应该保留人类的数学过程，只要它是可能的和谨慎的。我们相信，总的来说，我们越接近人类的过程，结果就越好-而且这些理想的特征（例如，“重要性”、“有用性”、“新颖性”等）将在结果中找到，而无需我们直接搜索或测量它们在这篇论文中，我们着重于确定数学家如何确定哪些真理被称为定理，哪些被搁置一边在这方面，我们发现了四个主要的性质，帮助数学家做到这一点。第一，每一个定理都应该满足至少在某种意义上是新的性质。接下来的两个性质是协同工作的;每个定理要么尽可能简单，要么提供比以前发现的任何定理更清晰的界限最后一个性质源于这样一个事实，即数学家倾向于选择逻辑等价，只要他们能得到它们因此，对于MATHsAiD所确定的每一个定理，以及所给出的每一个公理，系统都试图证明其逆命题，只要逆命题在某种意义上是一个实质性的命题。公平地说，这些想法都相当简单。我们认为，这是我们的方法的主要优点之一，因为往往是最简单的想法产生最好的结果。3.1已知vs新发现再考虑一个事实，对大多数逻辑学家来说，每一个被证明的陈述都应该被称为定理。这表明，就他们的思维而言，每一个真实的陈述都被认为是重要的（或不重要的），特别是，其他系统依赖于现有的ATP来提供许多用于确定“有趣性”，“有用性”，“新颖性”等的措施。ATP的有效性和效率，它们不捕获人类实践的数学过程。特别是，其他系统没有试图区分“数学”和“逻辑”。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2125其他真实的陈述。如果情况不是这样，那么人们会期望在不同类型的真理之间进行区分的术语。另一方面，数学家对他们认为是不同种类的真理有很多不同的名字（例如，引理，定理10，Corol-lary），表明数学家不仅要区分各种真理的重要性，而且要提供发现这些真理的历史感也就是说，引理11通常被称为引理11，因为它在证明定理时很有用，而推论通常很容易从定理中得出。然而，至关重要的是，大多数定理被数学家认为不值得任何特殊的名称。实际上，每个数学家都读过、听过或说过这样一句话：“很容易证明......"，或者声明，“这个结果是已知的”。虽然每一条线有时都以一种相当居高临下的方式使用，但它们背后的真理有助于强调逻辑学家当然，对一个数学家来说，“已知的”，无论如何都不简单地适用于那些已经发表的陈述。考虑一下数学家们的声誉，他们能够在看到一个定理时，相当快地推断出其他几个结论--比门外汉可能显而易见的还要因此，对于数学家来说，一旦一个定理被“新发现”，那么许多其他定理也立即成为“已知”的。由于这个原因，这些其他定理不被认为是新的定理12。为了方便起见，让我们假设“已知”的概念是明确定义的然后，我们可以建立一个由在时间t已知的陈述集合Kt组成的上升链，初始状态K0是由公理和逻辑规则组成的集合。如前所述，从数学家一组St（s所属）的语句，现在也变成了“新认识的”。因此，我们有K t+1= K t<$S t。应该指出的是，数学家不一定会宣布s，或就此而言，St的任何其他成员，是一个定理。诚然，“已知”的概念不仅s的选择是开放的，而且几乎可以肯定的是，数学家们对s的内容至少会有一些分歧。[10]在这一段中，定理一词指的是数学家赋予这个特定标题的陈述[11]必须指出，逻辑学家也引用引理。12除了偶尔的推论，就是这样。26R.L. McCasland等人/理论计算机科学电子笔记151（2006）21Kt+1，即使在s的选择上有一致意见。也就是说，数学家很可能会同意S t的基数几乎总是大于1，而逻辑学家可能会说S t的基数总是1。在任何情况下，实际上，我们不需要，也不想实际计算任何值t的集合K t或S t。我们的首要任务是确定，对于任何我们可能考虑称之为定理的陈述s，s不是毕竟，我们只是试图找到一种人类数学过程的3.2数学或逻辑数学家和逻辑学家都同意，证明的每一步都必须在逻辑上是合理的，同样，他们通常也同意证明中允许的论证类型事实上，这两个群体在所使用的证明步骤之间都有一定的区别，尽管数学家所做的区别可能比逻辑学家所做的要粗糙得多也就是说，两个群体都承认“逻辑”和“数学”证明步骤之间存在差异不同之处在于人们如何处理这些区别。一个数学家倾向于把逻辑仅仅看作是几种工具之一--毫无疑问，是一种不可缺少的工具--但它毕竟是一种工具。就像一个天文学家用望远镜，谁宁愿通过望远镜看，而不是在它，数学家喜欢研究数学，逻辑提供了一种手段，这样做。因此，从他们的有利地位来看，数学家不仅认为公理、逻辑和（已经发现的）定理是“已知的”，而且认为任何陈述都是从这些中的任何一个平凡地导出的粗略地说，我们所说的因此，在上面的符号中，一旦一个陈述s被证明，那么S t将包含所有从s平凡地导出的陈述，也许与Kt的任何代数组合。 或者换句话说，对于数学家来说，一个陈述是新的（因此，一个潜在的定理候选者），它的证明必须包含一些他们可以识别为数学的东西。因此，在MATHsAiD中，我们试图区分（作为数学家13作为目前如何在MATHsAiD中实现的一个例子，一旦已知交集的交换性和结合性，那么这两个属性的任何简单组合也是如此-例如，A（BC）=C（AB）。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2127在“逻辑”和“数学”证明步骤之间。因此，为了使任何被证明的陈述被报告为定理，它当然，这是一个必要的条件，但不是一个充分的条件。举一个非常简单的例子，我们再次考虑交集的交换性。显然，这个性质是逻辑“与”的交换性的结果。然而，对大多数数学家来说，“与”的可交换性不是一个定理（它只是逻辑上的！）。另一方面，交集的数学概念的可交换性是一个定理，因为交集公理和“and”的可交换性都没有3.3简单数学家总是希望语句以“最简单”的形式出现我们相信，他们的这种倾向不仅源于对现实本质的深刻理解- 但也是出于实际考虑。他们发现给某些概念命名是很有帮助的，特别是那些更有用的概念。换句话说，通过提供一个等价的，但更简单的形式，他们告诉对方他们认为什么是重要的。碰巧，它们也给了我们一种识别定理的方法--即简单性。在一类等价的陈述中，数学家通常选择最简单的一个--如果选择了任何一个的话--来记录为定理。当然，这条规则也有例外，我们将在下一节讨论其中一个例外然而，它不仅仅是数学家认为特殊的等价状态集合中最简单的一个。在发现的过程中，数学家可能会遵循一条特定的推理路线来证明许多陈述，其中可能很少有相互等价的。关于每个定理的简单性，所得到的定理序列可以有很大的不同。同样，在这个序列中，它通常是最简单的陈述，如果有的话，数学家选择称之为定理。所以，在《易经》中，我们只考虑“道”。[14]这条规则有一个例外;只要公理或定理的逆命题为真，那么这个逆命题也被报告为定理。参见第3.5节。15数学逻辑学家很可能不同意。但同样，这取决于一个人试图实现什么。毕竟，一个人28R.L. McCasland等人/理论计算机科学电子笔记151（2006）21最简单的陈述作为潜在的定理。简单性比较是在等价的语句之间以及在语句之一的证明列表16包含在另一个证明列表内的后一种比较代表了上面提到的推理路线。到目前为止，至少在接下来的两个部分中讨论了这个简单性规则的唯一例外定义3.1数学陈述S的简单性测度为了说明简单性比较，我们提供了两个例子。 [18]结果表明，当MATHsAiD找到结果A时，A=A（假设A是（A）A（A）A（A）A（A）后一个结果当然是从前一个得出的，事实上，它的证明列表包含了前一个结果人们可能假设这是它被丢弃的充分理由，而不是简单性测试失败的理由。下一个例子表明，情况并非如此。给定a，b∈G（其中G是一个群）和b∈a = e，MATHsAiD依次发现a−1等于e∈a−1，（b∈a）∈a− 1，b ∈（a ∈ a−1）和b ∈ e中的每一项。最后，它发现a-1= b。因此，最后一个等式的证明列表包含前面每个等式的证明列表，但是当然，最后一个等式是最简单的。3.4锐度在某些情况下，数学家喜欢的结果不一定是最简单的。其中一种情况涉及处理某种排序的语句。在这种情况下，通常优选更尖锐的边界定义3.2设f是集合S上的传递关系，且x，y，z∈S，使得x <$z和y<$z。然后说，y是一个（严格）比x（在z上）更尖锐的界限，如果x<$y和y<$x。例如，如果对于某些集合A、B和C，我们既有A <$B又有A <$C<$B，这是真的，那么数学家可能会想把后一个事实记录为定理，而忽略前一个事实--前提是A <$C不等于A。这种偏好的原因是，由于包含是一种偏序（或者更具体地说，是一种传递关系），并且由于我们总是有A<$A<$C，因此可以很容易地推导出16.一个列表，记录了给定陈述的证明所涉及的所有步骤[17]请注意，没有考虑任何函子的arity。事实上，我们曾尝试采用较复杂的方法。然而，这种相对简单的方法似乎效果最好。18相应的定理可以在附录中找到。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2129前者是后者。当然，反过来并不成立。注意，如果A<$C=A，那么上面的简单性规则应该适用，这意味着我们更喜欢前一个结果。在MathsAiD中，每当引入一个关系时，系统试图确定该关系是否满足人们在关系中寻找的通常性质;即，自反性，对称性，反对称性和传递性。如果关系被发现是传递的，但不是等价关系，那么默认设置（可由用户调整）是将此关系视为一种排序类型，并根据尖锐性而不是简单性来确定未来的定理。然而，这取决于一个条件（如上所述），即如果两项相等，则优先考虑较简单的一项。上述设置可以调整的原因是，对于更清晰的边界的偏好存在例外，这并不奇怪。例如，给定正整数a，b，c，d使得ab和cd，a+cb+d的结论被认为是定理，尽管存在更尖锐的结果，例如a+cb+c。<此外，在这种情况下，人们倾向于选择反向的边界例如，如果一个人知道A=B和B=C，那么他很可能会选择A=C作为定理，而不是其他两个陈述。这种选择通常是由，不考虑各自论点的简单性，而是考虑较弱的假设产生更强的，因此更有用的总体结果。3.5交谈在各种类型的定理中，数学家往往比大多数人更重视等价性。事实上，如果其中一个推论本身被认为不值得称为定理，他们通常愿意忽略它。当然，前提是它的反面被判断为能够独立存在。很简单，如果一个蕴涵和它的逆命题都为真，那么两者合在一起比单独使用更有用。由于这个原因，在MathsAiD中，只要一个蕴涵是已知的，无论是作为公理还是作为定理，那么就试图证明它的逆。第19章“合理的尝试” 事实上，大多数时候真的因此，应该在运用足够的努力来证明至少是常规结果，同时不要浪费太多的时间和努力来证明一些不正确的东西之间取得平衡30R.L. McCasland等人/理论计算机科学电子笔记151（2006）21如果这一尝试成功，则将逆定理作为定理添加20，而不考虑前面的任何条件。4结果到目前为止，我们已经在集合论、正整数（不带归纳法-在每种情况下，我们只探索了最基本的东西，但我们希望这是足够的，以便看到我们的定理滤波器工作得如何。MathsAiD从每个领域识别的定理请注意，由于不同作者之间风格的差异，我们同样允许教科书中定理的构成存在一些变化。当然，任何有特定标签的声明（例如，引理、推论等）也算在内此外，如果一个无标号的陈述以某种方式被分开，根据文本中建立的某种模式，以及陈述的某种证明，那么它也被算作一个定理。然而，练习不算作定理，虽然我们指出，当他们匹配无论是数学AID或另一本教科书除了MathsAiD发现的定理外，我们还包括在调查教科书中发现的每个定理（如上所述），这些定理可以合理地预期是由MathsAiD发现的，给出了公理21事实证明，MATHsAiD至少可以然而，出于本研究的目的，我们只对MATHsAiD在自动模式下生成的定理给予信任。应该注意的是，在某些情况下，提供给MATHsAiD的公理与本次调查中教科书中列出的公理有些不同。然而，就我们的目的而言，至少在所提供的例子中，这似乎并不那么相关。唯一的例外是在[9]中给出的交集的定义，它在相应的表中标记出来我们想指出的是，MATHsAiD和[20]当然，我们倾向于把等价作为一个定理，而不是两个独立含义中的任何一个。然而，对于本文，我们保留了结果，包括发现的顺序，就像MATHsAiD产生它们一样。21目前，用户还必须提供一些“例行”信息;例如，所涉及的谓词的类型，可以是关系、操作等。预计这在将来可以自动化。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2131每一本教科书似乎都与教科书本身的差异相当一致值得注意的是，当涉及到既有左手版本又有右手版本的定理时（例如，分配定律），MATHsAiD有时会产生两个版本，有时只产生一个版本。事实上，同样的现象也发生在教科书中。我们在下面的表格中提供了结果的摘要，但我们鼓励读者检查附录中记录的个别定理，并自行判断每个所谓的定理是否确实被公正地命名。在每个表格中，我们将MATHsAiD与两本教科书进行比较，并为每个定理来源给出两个分数这两个分数，如下所定义，以相同的方式计算，但使用略有不同的数据。在严格的评分中，来源必须几乎逐字记录定理，这在附录表格中的适当框中显示为一个勾。在更宽松的评分中，我们允许更多的差异，计算方框中的所有标记，除了T选择我们的评分系统主要是因为它的简单和公平。特别是，虽然它肯定是不公平的信贷给一个给定的来源，列出负载的所谓定理，没有其他来源呼吁该名称，它同样是不公平的其他来源，不惩罚给定的来源这样做同样，如果一个来源没有将其他两个来源都认定为定理的任何陈述认定为定理，那么这个来源也应该受到惩罚。请注意，在这个评分系统中，分数越高越好。我们希望MathsAiD的分数能与教科书的分数相媲美。也就是说，它的得分应该大致在其他两个范围内，它正在与之进行比较。下面的每个表都有以下键：sT（c）A（c）M（c）MAT定义4.1给定上述符号，在标准c下，每个源的得分由下式给出：得分（c）=（T（c）- 1.5A（c））-M（c）。[22]在每一种情况下，将MATHsAiD的发现归功于MATHsAiD似乎都不公平。- 但被抛弃了-定理然而，在G的情况下，例如，定理被过滤掉正是因为清晰度标准（用户可以调整32R.L. McCasland等人/理论计算机科学电子笔记151（2006）21集理论源T（s）A（s）M（s）评分T（g）A（g）男（克）评分（g）[9]第一章344523404628[12个]28411113141510垫4413420.5456333正整数源T（s）A（s）M（s）评分T（g）A（g）男（克）评分（g）[4]美国193113.5243118.5[10个国家]1106515078垫216210231021.5群论源T（s）A（s）M（s）评分T（g）A（g）男（克）评分（g）[1]第一章60247025[八]《中国日报》9107.59009垫80088017请注意，在六组分数中，MATHsAiD要么得分最高，要么得分第二好。5结论我们希望确定数学家确定哪些定理被指定为定理的各种标准，认识到这种将小麦与小麦分开的能力的重要性-不仅对数学家，而且对人工智能和机器学习系统也是如此然后，我们想把这些标准整合到一个自动化系统MATHsAiD中，这个系统同样可以区分这两种类型的真理，希望产生的结果可以与人类数学过程产生的结果相媲美为了检验我们的结果，我们将MATHsAiD给出的定理与各种数学教科书中的定理进行了我们认为，尽管仍有一些改进的余地，更不用说还有一些工作要做，R.L. McCasland等人/理论计算机科学电子笔记151（2006）2133但我们的努力总的来说是成功的。的确，我们到目前为止只研究了相当简单的数学结构，而且还只是入门级的。然而，这些结构彼此相当不同，但结果可以说至少在每个领域都是一样好的此外，我们的34R.L. McCasland等人/理论计算机科学电子笔记151（2006）21方法很简单确认作者谨此感谢各位裁判的宝贵意见和建议。引用[1] G. Birkho和S. MacLane，《现代代数概论》，第3版，麦克米伦纽约1965年[2] S. 《纯数学中的自动理论形成》，杰出论文系列，Springer-Verlag，伦敦，2002年。[3] J. Denzinger和S.陈文辉，知识型分布式演绎过程的研究，计算机科学，[4] C. W. Dodge，Numbers Mathematics，2nd Ed.，Prindle，Weber Schmidt，Inc.，一九七五年[5] J. Draeger和S. Schulz，通过无冗余的Lemmatization提高自动定理证明器的性能。在重症Russel和J. Kolen，编辑，第14届FLAIRS会议，基韦斯特，AAAI出版社，345[6] W M Farmer，J D Guttman，F J Thayer.小理论自动Springer Verlag，1992年。[7] 高耀，有趣定理的自动生成，硕士论文，迈阿密大学，2004。[8] T. W. Hungerford，Algebra，Holt，Rinehart and Winston，New York，1974.[9] K. Kuratowski 和 A. Mostowski ， Set Theory ， Studies in logic and the foundations ofmathematics，Vol. 86，Polish Scienti fic Publishers North Holland，Warszawa，1968.[10] E.朗道，《分析基础》，整体、有理数、无理数和复数的算术，切尔西，1951年。[11] D. Lenat，AM：一种人工智能方法来发现数学。斯坦福大学未发表的博士论文，1976年。[12] P. Suppes，公理集合论，Van Nostrand Reinhold，纽约，1960。A附录为了读者的方便，这里包含的所有数据都已用标准数学符号重写。除了一个例外（交集的定义），提供给MATHsAiD的公理/定义基本上与用于比较的教科书中的公理/定义相同。A.1集理论以下是提供给MATHsAiD的集合论公理/定义。R.L. McCasland等人/理论计算机科学电子笔记151（2006）2135公理：假设A和B是集合;1. 其中x∈/f ∈6。AB是一个SET2. 第七 集 A Set7 <$x，[（x∈Aorx∈B）<$$>x∈A<$B]3. [x，（x∈A=x∈B）]AB8. A是一个集合。四、 A=B[x∈B）]9. x∈A-B]5. [（x∈Aandx∈B）<$$>x∈A <$B]10. A-B是一个集合下表包含由MATHsAiD（MAT），[9]和[12]确定的集合论定理。假设A、B和C都是集合。定理[9]第一章[12个]垫1. 一辆皮卡。JJ2. AB和BA = B = A。JJJ3. AB和BC = AC。JJJ4. A.JJ5. AB和BAA = B。J六、 x，x∈/AJJ7. A A = A.JJJ8. A=。JJ9. BA=A B。JJJ10. （A B）C =A（B C）。JJJ11. AB A.JJJ12. 一个很好的。JJ13. AB = AB = A.JJJ14. AB = ACB C。GJ15. AB = CAC B。GJ16. CA和CB = CA B。DJ17. A A = A.JJJ18. A= A.JJJ19. BA=A B。JJJ20. （A B）C =A（B C）。JJJ21. AA B.JJJ22. BAB.JJ23. AB = AB = B。JJJ24. AB = ACB C。GJ25. AB = CAC B。GJ26. AC和BC = AB C。JJ27. A-A= 100。JJ28. A− A=A。JJ29. − A =J30. B−（A-B）= B。J36R.L. McCasland等人/理论计算机科学电子笔记151（2006）21定理[9]第一章[12个]垫31. （A-B）-A =。J32. A −（A-B）= A <$B。DEFJ33. （A-B）-B = A-B。J34. （A-B）-C = A-（B <$C）。JJ35. （A-B）<$（A <$C）= A-（B-C）。JJ36. A−BA。J37. AB = A-B =。JJ38. AB = A-CB-C。GJ39. （A <$B）<$（A <$C）= A<$（B <$C）。JRHVJ40. （A <$B）<$（A <$C）= A<$（B <$C）。JRHVJ41. （B <$C）− A = B <$（C −A）。JJ42. （B − A）<$（C − A）=（B<$C）− A。JJ43. AB = A = A B。JJJ44. AB = B = A B。JJJ45. A −（A <$B）= A − B。JJ46. A（A-B）= A-B。J47. （A-B）B = A B。JJ48. （A <$B）− B = A − B。J49. （A <$B）− B =。J50. （A-B）B =。J51. （A-B）<$（A-C）= A-（B<$C）。JJS52. （A-B）<$（A-C）= A-（B<$C）。JJ53. ABCD = ACBD。J54. ABCD = ACB D。J55. A<$B<$C<$D =<$A−D<$B− C。J56. CD = A-DA-C。JRHV-这个定理的G -这个定理的一个更一般的版本在正文中列出，并在表中给出（见定理53，54和55）。 考虑到适当的假设，MATHsAiD实际上找到了更一般的版本，但是由于锐度标准而丢弃它。D -这个定理的对偶（即第26条）在书中。DEFS -由MATHsAiD发现了右手边的一个更简单的等式（即定理34）。注意：我们还没有在MATHsAiD中实现一个系统，定理被修改/删除每当包容定理随后发现。因此，对于例如，定理2仍然存在，即使在定理5被发现之后。此外，如第4节所示，MATHsAiD有时会报告定理的左手和右手版本，而在其他时候只报告一个版本。这取决于各种因素，特别是提供给MATHsAiD的输入（包括公R.L. McCasland等人/理论计算机科学电子笔记151（2006）2137理），以前发现的定理，新定理本身的性质/结构，以及周围的情况。我们倾向于将这种行为视为一种假设-38R.L. McCasland等人/理论计算机科学电子笔记151（2006）21这是数学AiD的一个积极方面，因为这代表了一种在数学教科书中也可以观察到的现象（参见A.2中的定理10-21）。A.2正整数以下是提供给MATHsAiD的正整数的公理/定义（基本上如[4]中所示-没有归纳法）。(NOTE最后四个公理是第一作者另见群公理。）公理：设a，b，c∈N;1. N 是一组11。（a=b）<$（<$x∈Ns. t.）a+x=b）<$（<$y∈Ns.t. a=b+y）2. 1∈N12. a=b=0[（<$x∈N，a+x b）<$（<$y∈N，a/=b+y）]3. a+b ∈ N13. x∈N s. t. a+x=b=[（a/= b）n（n∈ N，ab+ y）]四、 a∈b∈N14.y∈Ns。t. a=b+y=[（a=/5. a+b=b +a a

下载后可阅读完整内容，剩余1页未读，立即下载