Mizar证明语言的人性化表示和详细的语义解释

理论计算机科学电子笔记174（2007）63-74www.elsevier.com/locate/entcs介绍和解释MizarJosef Urban1部查尔斯大学我都忘了。25，Praha，CzechRepublicGrzegorz Bancerek2比亚韦斯托克技术大学ul. Wiejska 45A，比亚韦斯托克，波兰摘要Mizar证明语言既有许多人性化的表示功能，也有严格的语义级别，允许严格的证明检查。 表示特性和语义对用户都很重要，理想的Mizar表示应该是人性化的（即非常接近教科书演示），并且还允许快速访问详细的语义和详细的证明解释。这提出了几个问题，问题和选择时，提出了原始的Mizar文本，提出了Mizar库的语义查询的结果，以及直接在语义层面上产生的文本时，例如，自动定理证明。本文讨论了这些问题的解决方案，特别是实现了一个初始系统，提供详细的解释原子Mizar推理。 这是通过Mizar XML表示工具、MML查询系统和自动定理证明器的合作完成的，这些自动定理证明器致力于Mizar的MPTP语义翻译。保留字：Mizar，校样展示，ATP，校样对象，MML查询，MPTP1引言Mizar [10，9]证明语言发展的主要目标之一一直是其直观的表达和接近数学语言。在这方面，以下特点值得• 它使用Jaskowski这些原子步骤被微调为“正确的他们应该1电邮地址：urban@kti.ms.mff.cuni.cz2 电子邮件地址：bancerek@mizar.org1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02264J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）易于理解的人类，但不应该打扰读者太多明显的细节。• 这种语言本质上是一阶谓词理论，但它支持许多语言特征，使其更像人类。这包括，例如，形容词和类型的使用以及它们的层次结构和依赖性的隐含使用（对于形容词称为“注册”或“簇”），各种属性（对称性、反射性、投射性等）的隐含使用，Mizar结构，隐含的定义扩展等。• 该语言支持各种各样的符号和几种符号重载，以允许在大型Mizar数学库（MML）中编码的不同数学领域的忠实符号。另一方面，拥有形式证明语言的主要目的是它们的机械化证明检查。这意味着所有上面提到的表示特性最终都必须转换到具有清晰语义的可验证级别。在Mizar中，这是在几个类似编译器的通道中完成的，这些通道逐渐将语法特征转换为它们的语义对应物（可能会通知用户语法错误等），并最终在语义层面上检查证明的正确性。1.1Mizar的语义层次Mizar语义层主要有两个转换• 公式被转换为Mizar范式（MNF），它只使用某些逻辑连接词（，<$，T和）。3• 将所有符号（符号及其模式）消歧到“构造函数”中。虽然前者通常非常复杂和重载，但构造函数是唯一的语义元素（函子，谓词等）。这两种转换都是多对一的，在某种意义上也是多对多的。多个用户级公式可以具有相同的MNF，并且多个用户级表示法最终可以在构造函数级上以相同的方式表示。至于多对多属性，理论上一个用户级公式可以有多个MNF，但实际上这不会发生，因为Mizar转换算法是确定性的。4将一个用户符号（符号及其模式）转换为不同的构造函数的可能性要大得多，因为这在很大程度上取决于Mizar环境（例如，类型规则有助于重载消歧的不同方式）。[5]这样做的重要后果是，给定一段语义级的Mizar文本，通常有多种方式可以呈现它。3 由Roman Suszko引入的术语[4]因此，如果我们将MNF定义为Mizar变换算法的乘积，那么它确实只是多对一。5 再一次，这只是多对一，如果我们修复特定的环境。J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）65这个语义层直接用于许多目的：它被Mizar本身用于证据检查和存储Mizar内部数据库。 它也用于MML Query [2]搜索和表示系统。 它也是MoMM [16]系统 、 Mizar Proof Advisor 和 MPTP [14 ， 17] 系 统中 使 用的 格式 的 基础 ， 以及MizarMode [15，3]中用于语义浏览的格式。应该注意的是，这个语义层仍然表示Mizar逻辑，而不是当前自动theo-rem prover（ATP）中使用的标准无类型一阶谓词逻辑，如E [12]，Vampire[11]，SPASS [20，19]，Otter [6]或Prover 9。当该逻辑被转换为标准谓词逻辑时，需要进一步处理：例如，Mizar类型需要被编码，Mizar隐式使用的所有知识（例如，类型层次结构）必须显式地表达等等。这现在由MPTP系统以某种方式（主要通过将类型编码为谓词来表征）完成然而，这种转换通常也是多对多的，在Mizar逻辑中通常会有多种编码纯谓词逻辑的方法。1.2使用语义级别进行链接表示最近，Mizar语义层已经完全XML化[18]，并且正在开发用于创建Mizar7的链接HTML表示的XML化的语义格式。XML化的语义格式已经被设计成使得符号和其他Mizar资源的HTML链接相对容易，并且它已经被修改了几次（通常通过添加额外的信息作为XML属性），使用HTML表示瓶颈作为反馈。它目前允许相当忠实地重新创建原始的Mizar表示（更多细节见第3节），同时它也揭示了Mizar系统计算的许多信息（例如隐式计算的各种公式-用于说明Mizar属性，正确性条件等），这通常是Mizar作者无法访问的。使用纯JavaScript 创建HTML 表示的 主要原因是 ，目前 所有主流浏 览器都支持JavaScript语言。这意味着Mizar作者现在可以在创作过程中随时将XML文件（Mizar验证的副产品）直接加载到浏览器中，从而立即获得其中包含的所有附加信息。然而，Mizar文章的XML化形式（以及HTML演示文稿）并不包含任何对原子“简单调整”（“by”）步骤的解释这种解释对于开光处理本身的任何目的都是不需要的，它的添加（即，为“简单公正”步骤的证明检查提供文档模式这意味着到目前为止，用户无法找出为什么特定的原子步骤被Mizar接受。如上所述，这些步骤被设计为对人类来说6http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/miz.xsltxt?视图=标记7http://merak.pb.bialystok.pl/mml/66J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）然而，这是一个非常主观的问题，取决于许多因素。与正常的自然语言证明一样，有时在原子Mizar步骤中使用的“明显”事实的数量对于读者来说人类也善于偶尔忘记应该是显而易见的。Mizar对数学形式化领域的最大贡献之一与战术证明器不同，该语言不应该是“只写”的）。虽然可读性本身是一个非常有价值的目标（好吧，为什么所有的数学不应该以一种可读的，但形式上正确和机械检查的方式呈现呢语言的这个特征实际上在维护像今天的MML这样的大型形式数学库中，以及对于它的重构（例如，概括，重新制定整个理论，等等）。出于所有这些原因，提供一个可选的更精细的解释级别，这有助于在必要时理解更困难的步骤，应该是有用的。1.3本文的其余部分我们描述了我们最初的解决方案，提供和呈现Mizar原子“简单公正”推理步骤的解释。该解决方案（cf.图1）使用ATP技术（现在的E-PROVER）提供实际的解释作为ATP证明对象。MPTP系统用于将Mizar“简单证明”推理步骤转换为ATP问题，而MML查询系统用于将ATP证明对象转换回Mizar符号。然后，由MML Query转换的证明对象链接到Mizar文章的HTML表示中的适当位置，以便用户在不清楚特定原子推理步骤时可以轻松访问它们。这种处理需要上述多对多转换中的几个（主要是以与上述相反的顺序）。我们解释了MML查询所使用的一般算法，用于以用户友好的符号表示任意语义级公式。该算法通常用于呈现MML查询搜索结果，我们现在也使用它来呈现由ATP直接在语义级别上创建的文本。MML查询解决方案，这个表示的问题相比，在HTML表示的Mizar文章中实现的解决方案，并讨论其适用于不同的目的。2解释和介绍Mizar简单的正义读者可以在作者的网站8上查看解释Mizar原子推理的功能（现在已为35篇最初的Mizar文章实现这是Mizar HTML演示文稿的开发版本，非常类似于8http://lipa.ms.mff.cuni.cz///www.example.com/xmlmml/html bytst/J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）67图1.一、 用于呈现Mizar原子步骤的系统图一个在开阳星9号目前的主要区别是关键字by的链接，这导致了MML查询呈现的ATP证明对象，也可以在我们的站点10上获得。我们在下面提供一个简单的例子。2.1从用户角度看的简单例子例如，考虑Mizar文章ZFMISC 1[4]中的第一定理11：定理Th 1：ZFMISC_1：1 bool {}= {{}}证明现在设c1为设定值;（c1 c={}当且仅当c1 ={}）;因此（c1inbool {}iffc1in{{} }）由Def 1，TARSKI：def1;结束;9http://mmlquery.mizar.org/mml/4.48.930/www.example.com68J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）http://lipa.ms.mff.cuni.cz/http：//www.example.com字节/通过/11 http://lipa.ms.mff.cuni.cz/搜索urban/xmlmml/html bytst/zfmisc 1.html#T1J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）69因此bool {} = {{} } by TARSKI：2;end;它的自然语言解释（可能是多余的）是空集的幂集是一个只包含空集的单例在证明中使用的符号表示集合论成员，下面使用的符号c=表示集合论包含。 注意，定理XBOOLE1：3 12定理E3：XBOOLE_1：3对于b1被设置成立（b1 c={}意味着b1 ={}）只是一种暗示，而不是等价所以用户可能想知道，为什么第一个推论13（c1 c={}当且仅当c1 ={}）;在逻辑上是有效的。点击其关键字将显示由MML查询15呈现的以下E-PROVER第一个公理是自反性r1塔斯基，说明包含谓词的自反性。这是Mizar属性，系统会自动使用，假设这对读者来说是显而易见的。有了这个公理，推论就很容易得出：MML查询 ATP证明步骤的呈现axiom：reflexivity_r1_tarskiA：步骤1对于x1，x2被设置，则x1 c= x1推测：e1_10_1 A：第7（c11001 c={}森林论坛c11001 ={}）axiom：t3_xboole_1 A：步骤8对于x1被设置stx1 c= {}保持x1 ={}推理：assume_negation（7）A：步骤9（c11001 c={}c11001>{}或c11001 ={}而不是c11001 c={}）&&inference：variable_rename（1）A：步骤11对于x3，x4被设置保持x3 c= x3推理：split_conjut（11）A：步骤12 x1 c=x1推理：fof_nnf（9）A：步骤22（c11001 c= {}表示c11001> {}）&12http://lipa.ms.mff.cuni.cz/http：//www.example.combytst/xboole1.html#T313 http://lipa.ms.mff.cuni.cz///www.example.com/xmlmml/htmlbytst/zfmisc1.html#E1:10114 http://lipa.ms.mff.cuni.cz/http：//www.example.com/xmlmml/html bytst/ by/zfmisc 1/164 29.html[15]请注意，我们的系统已将常数c 1重命名为c 11001。 这实际上是c11001在HTML中的渲染，下标编码了当前的Mizar校对级别。这是MPTP系统命名约定的结果，它需要为每个MPTP对象提供唯一的名称70J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）（c11001 c={}或c11001 ={}）推理：split_conjut（22）A：步骤23（c11001 ={}或c11001 c={}）推理：split_conjut（22）A：步骤24（c11001 = {}表示不是c11001 c={}）推理：fof_nnf（8）A：步骤25对于x1被设置stx1 c= {}保持x1 ={}推理：variable_rename（25）A：步骤26对于x2被设置stx2 c= {}保持x2 ={}推理：split_conjut（26）A：步骤27（x1> {}表示不是x1 c={}）推论：csr（24，27）A：步骤29不是c11001 c={}推论：sr（23，29）A：步骤30c11001 ={}推理：rw（rw（29，30），12）A：第31步矛盾2.2简单的例子进一步解释现在我们将解释创建和渲染ATP解释的特定阶段。2.2.1ATP问题这些问题是由MPTP系统的开发版本产生的。这是一个将Mizar转换为无类型一阶谓词逻辑的系统，并以适合ATP系统解决的方式编码Mizar问题。该系统的最新（第二）版本已经经过了相当严格的测试（见[17]），对于不包含可能的算术评估的问题（这将需要进一步处理），它现在似乎提供了所有必要的信息，以便由ATP进行Mizar推理如上所述，MPTP将Mizar类型编码为谓词，并显式地向问题规范添加各种对Mizar来说显而易见的信息（如类型层次结构或反显性属性上面提到的）。ATP问题规范（文件名为zfmisc 1 164 29，使用TPTP [13]格式）如下：% Mizar问题：e1_10_1，zfmisc_1，164，29 fof（reflexivity_r1_tarski，axiom，（！[A，B]：r1_tarski（A，A）），file（tarski，r1_tarski），[]）。fof（dt_k1_xboole_0，axiom，$true，file（xboole_0，k1_xboole_0），[]）. fof（dt_c1_10_1，axiom，$true，file（zfmisc_1，c1_10_1），[]）. fof（fc1_xboole_0，axiom，v1_xboole_0（k1_xboole_0），file（xboole_0，fc1_xboole_0），[]）. fof（rc1_xboole_0，公理，（？[A]：v1_xboole_0（A）），file（xboole_0，rc1_xboole_0），[]）.fof（rc2_xboole_0，公理，（？[A]：~（v1_xboole_0（A），J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）71file（xboole_0，rc2_xboole_0），[]）. fof（e1_10_1，猜想，(r1_tarski（c1_10_1，k1_xboole_0）=> c1_10_1=k1_xboole_0），inference（mizar_bg_added，[]，[reflexivity_r1_tarski，dt_k1_xboole_0，dt_c1_10_1，fc1_xboole_0，rc1_xboole_0，rc2_xboole_0，t3_xboole_1]），[file（zfmisc_1，e1_10_1）]）。fof（t3_xboole_1，公理，（！[A]：（r1_tarski（A，k1_xboole_0）=>A=k1_xboole_0）），file（xboole_1，t3_xboole_1），[]）.这种编码在[17]中有更详细的描述。请注意，这里有比上述证明实际需要的更多的公理。这是因为用于添加“背景知识”的MPTP算法2.2.2创建ATP证明Mizar简单正义产生的MPTP问题对于当前的ATP系统来说通常我们使用的是Stephan Schulz的E-PROVER的最新版本（0.91），这既是因为它的强大，也是因为它支持TPTP标准，这允许我们使用TPTP工具进行预处理和后处理。通过SystemOnTPTP16运行E-PROVER会产生以下TSTP证明对象：fof（1，axiom，！[X1]：！[X2]：r1_tarski（X1，X1），file（'/tmp/SystemOnTPTP15237/zfmisc_1 e1_10_1.p'，reflexivity_r1_tarski））.fof（7，consumption，（r1_tarski（c1_10_1，k1_xboole_0）<=>equal（c1_10_1，k1_xboole_0）），file（'/tmp/SystemOnTPTP15237/zfmisc_1 e1_10_1.p'，e1_10_1））.fof（8，axiom，！[X1]：（r1_tarski（X1，k1_xboole_0）=>equal（X1，k1_xboole_0）），file（'/tmp/SystemOnTPTP15237/zfmisc_1e1_10_1.p'，t3_xboole_1））.fof（9，negated_conjecture，~（（r1_tarski（c1_10_1，k1_xboole_0）<=>equal（c1_10_1，k1_xboole_0），inference（assume_negation，[status（cth）]，[7]））.fof（11，plain，！[X3]：！[X4]：r1_tarski（X3，X3），inference（variable_rename，[status（thm）]，[1]））.cnf（12，plain，（r1_tarski（X1，X1）），inference（split_conjunt，[status（thm）]，[11]））. fof（22，negated_conjecture，（（~（r1_tarski（c1_10_1，k1_xboole_0）|~（equal（c1_10_1，k1_xboole_0）&（r1_tarski（c1_10_1，k1_xboole_0）|equal（c1_10_1，k1_xboole_0），inference（fof_nnf，[status（thm）]，[9]））。cnf（23，否定猜想，（c1_10_1=k1_xboole_0| r1_tarski（c1_10_1，k1_xboole_0））、推断（split_conjut，[status（thm）]，[22]））。cnf（24，否定猜想，（c1_10_1！= k1_xboole_0| ~r1_tarski（c1_10_1，k1_xboole_0））、推理（split_conjut，[status（thm）]，[22]））。fof（25，plain，！[X1]：（~（r1_tarski（X1，k1_xboole_0））|equal（X1，k1_xboole_0）），inference（fof_nnf，[status（thm）]，[8]））。fof（26，plain，！[X2]：（~（r1_tarski（X2，k1_xboole_0））|equal（X2，k1_xboole_0））、inference（variable_rename，[status（thm）]，[25]））。cnf（27，普通，（X1=k1_xboole_0| ~r1_tarski（X1，k1_xboole_0）），inference（split_conjut，[status（thm）]，[26]））.cnf（29，negated_consumption，（~r1_tarski（c1_10_1，k1_xboole_0）），inference（csr，[status（thm）]，[24，27]））.cnf（30，negated_conjecture，（c1_10_1=k1_xboole_0），inference（sr，[status（thm）]，[23，29，theory（equality）]））.cnf（31，negated_consumption，（$false），inference（rw，[status（thm）]，[推理（rw，[状态（thm）]，[29，30，理论（平等）]），12，理论（平等）]））。cnf（32，negated_consumption，（$false），inference（cn，[status（thm）]，[31，theory（equality）]）。cnf（33，negated_consumption，（$false），32，'proof']）.显然，不同的ATP系统（或者甚至是具有不同设置的相同ATP运行）可以产生不同的反驳证明，并且这些证明通常也不同于假设的Mizar检查器完成的步骤16 http://www.cs.miami.edu/httptp/cgi-bin/SystemOnTPTPFormMaker72J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）以证明猜想的正确性）。当然，我们可能会尝试优化搜索，以找到例如，最短的（因此希望是“最好理解的”）证明。 另一方面，如上所述，这些推理对人类来说应该是很容易的，而且对ATP来说也很容易，所以这种（可能是相当资源密集型的）优化可能不值得付出代价。使证明更容易理解的一个更好的方法是花一些时间来展示它们，这就是我们在下面的步骤中所做的2.2.3为MML查询呈现TSTP证明对象首先被Petr Pud l a `k和G eo Put Sutchee的T P T P2XML转换为TSTP的XML编码。 XML清单将长期包含在这里，并且可以在我们的网站上获得。然后，我们应用我们的MySQLtstp2dli.xsl 18，它将TPTP表示法转换为MML查询DLI（解码库项目）格式。MML Query仅用于处理DLI编码的公式，因此tstp2dli.xsl的另一个任务是负责将公式名称链接到Mizar HTML页面，以及ATP步骤引用的链接。结果再次在我们的网站19.2.2.4使用MML查询表示如上所述，MML查询DLI格式是Mizar语义级别的表示法。因此，MMLQuery必须完成两项任务：• 将MNF中的公式翻译回人类友好的符号（即，通常通过使用更多的逻辑连接词来压缩它）• 将Mizar构造函数转换回人类友好的符号（即，找到合适的Mizar符号和它们的模式，它们对应于给定的构造函数形式）首先，我们解释MNF转换。MML Query中使用的MNF中的合取词可能有两个以上的合取词（Mizar中合取词的结合性的结果）。这种情况在这里用&（. . ）.更丰富的连接词集（，和惠）的重建试图逆转Mizar变换算法，可以通过以下规则来描述：<$x→ x <$&（，<$n−1，<$$>n）→&（<$1，.，n−1）n<$（&<$1，.，<$n）→1. 巴恩惠的重建有点复杂。如果公式的形式是&（，k，k−1，.，<$$>n）<&$1，.（2000年，100万美元）和&（&（），1，.，k）&1，.（2000年，100万美元）17http://lipa.ms.mff.cuni.cz/http：//www.example.com通过XML/zfmisc1/16429.xml18http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/tstp2dli.xsltxt?view=markup19 http://lipa.ms.mff.cuni.cz/http：//www.example.com http：//www.example.comJ. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）73然后它被转化为&（2011年1月1日，.，k）惠<$&（k+1，. ，n）等价项是满足双重否定和单合取条件的最小等价项：和（）Quniifenienisisioapp i enieni s i s于2013年12月31日，本集团（“本集团”）的资产负债表列示如下：为了更好的可读性，对长公式进行了缩进和中断。上述规则假设，公式不包括双重否定，也不包括嵌套或单连词（这是从Mizar生成的公式的情况）。因此，用、<$、T和表示的任意公式的变换需要在开始时进行额外的修剪这已经被实现来处理我们的ATP生成的数据。将Mizar构造函数翻译成人类友好的符号使用“第一可用符号规则”。通常，多个同义词（或反义词）可以作为对应于一个Mizar构造函数的用户符号存在（换句话说，当Mizar作者引入同义词时，它只存在于表示层）。由于在一般情况下（比如数据来自ATP），除了构造函数格式之外，我们没有其他信息，因此使用MML中找到的第一个人类符号来表示构造函数是合理的，它对应于该构造函数。当附加信息可用时，MML查询可以（并且已经）使用更多特殊规则，例如，关于构造函数编码的Mizar文章。我们的示例的最终MML查询渲染步骤的结果已经在上面显示，它是呈现给读者的“简单公正”推断的最终解释3MML查询表示与基于XML的全文HTML表示上面描述的解释系统，我们已经实现了35个初始的Mizar文章，使用两种不同的技术来呈现Mizar语义级别。通过MML查询“人工智能”重建可能的用户符号（在2.2.4中描述）来呈现附加解释在构造函数编码中没有添加其他信息的情况下，实际上没有其他选择。另一方面，对于基于XML的完整文档的HTML表示，MML查询解释链接到它，可以获得许多进一步的尽管MizarXML格式的目的主要是包含语义信息，但XML格式允许轻松添加原始表示信息。此功能已添加到Mizar一段时间74J. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）以前，由最近发布的Mizar版本生成的XML已经包含了这些额外的表示信息。因此，很可能在许多情况下，这两个系统对同一个Mizar公式的表示会有所不同。我们基于XML的HTML表示的目标是实现与原始文章的高度相似性，并尽可能多地添加语义信息，而MML Query表示的目标是以统一和可预测的方式表示Mizar文本片段。 从这个意义上说，MML查询表示可以被认为是Mizar强大统一格式的工具。虽然这种差异最初可能会让读者感到惊讶，但当他第一次使用解释功能时，这也可能会让他更深入地理解演示过程和Mizar本身。如果这成为一个严重的问题，我们可以随时向用户提供将MML查询格式应用于整个基于XML的文章表示。4结论和今后的工作我们已经提供了一个解释Mizar原子“简单公正”推论的系统的初始实现为此，我们使用或新开发了一系列在Mizar语义层面上工作的工具。该系统现在已经可以扩展到MML的更大部分，因为ATP解决非数值Mizar“简单正义”问题的成功率（17）。然而，我们仍然没有一个令人满意的算法，认真转换的ATP解决方案的重类型的Mizar文章的Mizar类型的语义水平。现在已经可以使用上面提到的MML Query呈现这样的解决方案，并且它可能纯粹用于解释目的。然而，从Mizar解析器的角度来看，这样的呈现是将ATP非类型化解转化为Mizar可接受的类型化解可能是可行的，这是进一步研究的一条有趣的路线。显然，参与我们链的所有工具都可以改进。一个有趣的想法是让所有参与链的系统实时工作，相互传递解决方案。这种功能可能很快就会开发出来，通常用于为Mizar作者提供ATP支持。 从这个角度来看，提供当前的解释功能可以被认为是一个测试平台，为更雄心勃勃的ATP-for-Mizar应用程序铺平道路。5致谢该公司致力于开发和提供参与我们工具链的ATP系统和元系统。GeoJ. 厄本湾，澳-地Bancerek/Electronic Notes in Theoretical Computer Science 174（2007）75Sutzarie还首次在Mizar HTML演示文稿中建议了这项工作得到了第六届欧洲共同体框架计划内的玛丽·居里国际奖学金的引用[1] Andrea Rupti，Grzegorz Bancerek，and Andrzej Trybulec，editors. 数学知识管理，第三届国际会议，MKM 2004 ， Bialowieza ， 波 兰 ， 2004 年 9 月 19 日 至 21 日 ， 会 议 记 录 ， 计 算 机 科 学 讲 义 卷 3119 。Springer，2004.[2] Grzegorz Bancerek和Piotr Rudnicki。MML中的信息检索。在MKM，第2594卷，计算机科学讲义，第119-132页。Springer，2003年。[3] Grzegorz Bancerek和Josef Urban。Mizar Mathematical Library的集成语义浏览，用于创作Mizar文章。在Liechti et al.[1]，第44[4] 切斯拉夫·拜林斯基 集合的一些基本性质。 Formalized Mathematics，1（1），1989.[5] S.贾斯科夫斯基 关于假设的规则。 Studia Logica，1，1934.[6] W. W. 麦库尼Otter 3.0参考手册和指南。技术报告ANL-94/6，阿贡国家实验室，伊利诺伊州阿贡，1994年。[7] 亚当·瑙莫维奇和切斯拉夫·拜林斯基用属性和要求改进mizar文本。在Liechti等人[1]，第290-301页中[8] F. J·佩尔蒂埃 自然演绎简史。 逻辑的历史和哲学，20：1[9] 彼得·鲁德尼基和安杰伊·特里布勒克。关于有根据的等价物。J. Autom. Reasoning，23（3-4）：197 -23 4 ， 19 9 9 .[10] P. 鲁德尼基Mizar项目概述在1992年的研讨会上类型的证明和程序，第311-332页查默斯理工大学，巴斯塔，1992年。[11]亚历山大·里亚萨诺夫和安德烈·沃龙科夫。VAMPIRE的设计与实现。 Journal of AI Communications，15（2-3）：91[12] S.舒尔茨 天才定理证明者。 Journal of AI Communications，15（2-3）：111-126， 2002.[13] G. Suttagrabe 和C.B.萨特纳TPTP 问题库：CNF 版本v1.2.1。Journal of Automated Reasoning，21（2）：177[14] 约瑟夫·厄本MPTP -动机，实施，第一次实验。Journal of Automated Reasoning，33（3-4）：319[15] Josef 城市。 MizarMode - 集成 证明辅助 工具为 开阳之路 正式确定数学应用逻辑杂志，2005年。出版中的文章，doi：10.1016/j.jal.2005.10.004，可在http://ktiml.mff.cuni.cz/网站mizmode.ps查阅。[16] 约瑟夫·厄本 MoMM -快速interreduction和检索大型图书馆的形式化数学。International Journal on Arti Ficial Intelligence Tools，15（1）：109[17] 约瑟夫·厄本MPTP 0.2：设计、实现和初始实验。自动推理杂志，2006年。接受出版。[18] 约瑟夫·厄本Mizar的XML化：简化MML的语义处理和表示。Michael Kohlhase，编辑，MKM 2005，Lecture Notes in Arti Ficial Intelligence，第3863卷，第346-360页。施普林格，2006年。[19] Christoph Weidenbach ， Uwe Brahm ， Thomas Hillenbrand ， Enno Keen ， Christian Theobald ， andDalibor Topic. SPASS 2.0版。2002年，第275-279页[20] C.魏登巴赫《自动推理手册》，第二卷，第SPASS章：组合叠加、排序和分裂，1965-2013页Elsevier andMIT Press，2001.[21] 弗里克·韦迪克检查器 - 注意到对的基本推理迈扎尔提供http://www.cs.kun.nl/，2000年。