Logiweb：存档、检索、传输、验证数学，简单、连贯、万象系统，高质量论文可机器验证

理论计算机科学电子札记93（2004）70-101www.elsevier.com/locate/entcsLogiweb克劳斯·格鲁1哥本哈根大学计算机科学系（DIKU）丹麦摘要本文介绍了一个软件系统的初步名称为“Logiweb”，这是试图设计一个简单的，连贯的，包罗万象的系统的存档，检索，传输，分发，验证，并表示数学。该设计是从零开始的，但在很大程度上取决于现有系统的经验和现有技术的当前阶段Logiweb确保页面一旦发布，在未来保持不变，以便从数学论文中引用Logiweb页面是安全的。在这一点上，Logiweb补充了万维网，它更适合于在Linux中的数学。关键词：证明检查器，数学档案，数学检索，记法自由，协议，数学知识管理1介绍Logiweb是一个类似网络的系统，允许逻辑学家在网络上发布具有高排版质量和高人类可读性的论文，这些论文也是机器可验证的。除此之外，Logiweb允许论文包含形式理论的定义此外，Logiweb允许论文在互联网上相互引用，并允许对跨越世界上不同地方的几篇论文进行证明检查。例如，一篇论文中的引理可能引用了另一篇论文中定义的结构，在这种情况下，证明检查器必须访问这两篇论文来确定证明的正确性。1 电子邮件地址：grue@diku.dk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.029K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-71除此之外，Logiweb为存档数学提供了一种媒介。它可以按原样使用，也可以在其他系统（如Mizar）下安静透明地运行[12，16]。相比之下，万维网通过MathML和OMDoc [10，11]支持数学，是一种适合于在Linux中的信息的媒介。Logiweb给予用户完全的符号自由，以及选择任何公理理论（例如ZFC）作为其工作基础的Logiweb还允许不同的符号系统和理论共存并顺利互动。Logiweb最初设计用于支持地图理论[2，7，15，17]，它与ZFC具有相同的功能，但依赖于非常不同的基础，例如，它依赖于λ演算而不是一阶谓词演算。然而，与地图理论的联系已经被打破，因为Logiweb同样很好地支持所有公理化理论。Logiweb从基于谓词演算的理论（如ZFC）扩展到基于λ演算的理论（如Map Theory）的能力保证了Logiweb对逻辑没有任何限制。没有这样的限制，当然不可能提供一个代码从定理提取设施，如Nuprl [4]的术语，但用于操作定理和证明单个理论的功能可以用Logiweb的编程语言表示Logiweb的程序设计语言是嵌入在Map Theory中的程序设计语言，它使得利用Map Theory对 Logiweb进行推理成为可能。Logiweb允许个人发表论文，但也允许期刊存在。从技术上讲，期刊问题将只是一个Logiweb页面，引用已接受的论文。然而，在社会上，期刊编辑可能会对作者执行排版、风格、符号使用等方面的指导方针，以确保期刊内部的一致性和与标准文献的一致性Logiweb本身对这些要求是中立的，一种期刊的指南不会限制其他期刊，也不会限制引用期刊的作者的标注自由。1.1发展历史Logiweb大量借鉴了其他证据系统的经验。在许多来源中，Logiweb基于作者1985-1992年实现的证明检查器Logiweb的一个目标是设计一个简单的证明系统，以应对数学教科书的复杂性。为了确保该系统能够以人类可读的方式处理完整的数学教科书的复杂性，1992-2001年开发了两本书[8，9]来测试72K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-the system.参考文献[8]是一本面向大学一年级学生的离散数学书，在这里很感兴趣，因为它可以在实践中测试这本书的人类可读性。参考文献[9]是一篇关于映射理论的论文，这里很感兴趣，因为它包含了一个可以对Logiweb进行压力测试的实质性证明（ZFC在映射理论中的一致性证明）。为了允许与其他证明系统进行比较并确保正确性，[9]已经手工移植到Isabelle [13，14，15]。写作[8，9]的一个目的是确定数学知识管理系统必须具有的语法和语义特征除其他外，第6节中介绍的宏观设施是为了应对这些需求而开发的Logiweb目前由学生使用，他们使用Logiweb已经实现的部分面向更广泛受众的实验版将于明年年初推出。1.2文件概述论文的各部分从简短的介绍开始，其中包括重新标记，动机，以及与与给定部分相关的一些文献的比较。第2节给出了Logiweb对用户来说是什么样子的简短示例。 对于500页和300页的例子，分别参考[8]和[9]。第3节描述了Logiweb如何确保页面在发布后保持不变并在未来可用，以便从数学论文中引用Logiweb页面是安全的。第4介绍了Logiweb中的主要数据结构：（1）描述页面结构的解析树，是Logiweb存储的实体。(2)从解析树中提取的代码，以更详细的方式机器可理解的数据库格式。(3)代表概念的符号。(4)方面，它允许符号在不同的上下文中具有不同的含义。第5描述了Logiweb如何确保符号自由，基础自由和独立的个人作者，同时支持相互依存，允许作者相互引用，使用彼此的成果。第6描述了Logiweb的宏工具，它允许保持de Bruijn因子[5]较低，并支持页面是人类和机器K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-73函数f（x）由y[f（x）=stecx2−1]定义。Wehave[f（10）=99].阅读与此同时第7描述了Logiweb的编程语言。Logiweb的编程语言是嵌入在Map Theory[2，7，15，17]中的编程语言，它允许Logiweb使用Map Theory（具有ZFC功能）来推理Logiweb。第8描述了Logiweb如何进行页面验证，并描述了如何将Logiweb的默认正确性标准更改为例如Mizar [12，16]正确性标准，从而允许在其中嵌入其他系统。Logiweb。第9描述了如何引导系统，该系统在一个系统中是非平凡的，该系统具有完全的记法自由，因此，不能依赖于任何具有任何预定义语法的构造。附录A描述了Logiweb服务器之间用于存储和检索未解释的Logiweb页面的字节级协议。附录B描述了Logiweb浏览器用于解释Logiweb页面的协议。2入门从实现者的角度来看，Logiweb是一个协议，但从用户的角度来看，Logiweb是一个“Logiweb页面”的集合 要使用Logiweb，用户需要一个Logiweb浏览器以及对存储页面的Logiweb服务器的Internet访问。以下部分描述了在不同站点工作的两个人B和C如何使用Logiweb进行合作2.1定义和声明一个最小的例子是，最大posePersonB不需要定义f（x）=stecx2−1在LogiWeb上。 B可以通过发布一个（非常短的）页面就像这样：方括号指导正确性检查：方括号中的文本应由校对检查器读取。方括号外的文字为评注。人C可能会找到BC可以通过发布另一个页面来这样做：74K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-Definne[f（x）=stecx2−1]和[f（x）=stecx2−2]。[RuleP0：（x）x+0 =x][RulePJ：（x，y）x+yJ=（x+y）J][Rule传递性：（x，y，z）x=y<$x=z<$y=z][理论yS+：P 0<$P<$Transitivity][S+lemmaL2.3.1：x=x+0]J每一页都包含一个参考书目（不需要可见）。上面，后一页必须引用前一页，以表明后一页上的f（x）是前一页上定义的。反过来，前一页必须提到pagesthatdefinexy，x−y，x=stecy，and ndnumer a ls.2.2正确性一个页面可能是“正确的”或“错误的”。Logiweb浏览器必须能够“验证”页面（即检查页面是否正确）。 上面几页是正确的，第一是因为它的定义是可以接受的，第二是因为它的主张是正确的。上面的两页位于世界上不同的地方。为了验证后一个页面，Logiweb浏览器必须访问这两个页面以获得定义和声明。根据Logiweb默认标准，页面是正确的。页面可以通过指定替代标准来覆盖默认值作为一个例子，你可以把一篇Mizar [12，16]论文放在Logiweb上，并根据Mizar标准指定它是正确的。关于正确性标准的细节将在后面给出根据默认标准，和Wehave[f（10）=100].这两个定义都是错误的，第一是因为这两个定义相互矛盾，第二是因为它的主张是错误的。2.3引理与证明默认正确性准则允许定义规则和理论，并陈述和证明引理。假设用户B发布了以下页面：K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-75[L2.3.1的证明：L1：P0L2：P0x+0 =x;x+0 + 0 =x+0;L3：传递性DL2D L2x +0 =x+0;L4：传递性DL1D L3x =x+0]该页将P0定义为对于所有项x，x+0 =x的规则，PJ是对于所有项x和y，x+yJ=（x+y）J的规则，传递性是如果x=y和x=z，则对于所有项x，y和z，y=z的规则。则page definesS+ 是以P0，PJ和传递性为公理和推理规则，并陈述为引理L2.3.1，x=x+ 0是定理S+。在最后一行中，x服务于一个概念变量;在这三个概念中，x服务于一个然后C可能决定在另一页上证明x=x+0同样，这两个页面位于世界上两个不同的地方，检查第二个页面需要访问这两个页面。作为一个技术性的注释，第一页是正确的，根据“局部正确性”的默认标准，它只要求证明是正确的，但不要求所有引理都有证明。用户可以选择更严格的3稳定性当作者引用一篇论文时，作者通常希望引用的论文保持稳定（即不变），并在未来可用。本节介绍Logiweb如何满足坚固性和可用性的稳定性要求。3.1坚定性当一个页面被发布时，一个“Logiweb引用”被分配给该页面。引用是一个大约200位的自然数，由RIPEMD-160散列密钥、时间戳和版本号组成，但用户看不到引用。现在假设上面的前两页分别由B和C发布时得到引用9··· 91和9··· 9276K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-Wehave[f（10）=99].函数f（x）由y[f（x）=stecx2−1]定义。9··· 91（B9··· 92（C在出版时，C[f（x）=stecx2−1]到e。G. [f（x）=stecx2− 2]，那么C的页面就会出错。然而，在Logiweb上，一旦发布，就不可能更改页面PersonBcanofcourseni shapagethatsays[f（x）=stecx2−2]，但页面将得到一个新的引用，如9··· 93，而9··· 92页仍参见第9 ···91页。页面的引用基于RIPEMD-160哈希码，该哈希码是基于页面的所有内容计算的。只要RIPEMD-160能够抵御冲突攻击，即使是恶意用户也无法更改发布后的Logiweb页面。没有两个用户能够发布获得相同引用的不同页面Logiweb服务器的任务是维护一个将引用转换为页面的全局哈希表。正如在摘要中提到的，Logiweb是存档数学的媒介。换句话说，Logiweb是累积的，一旦一个页面放在Logiweb上，就不可能改变它。这种累积的性质是由RIPEMD-160强制执行的。3.2可用性即使Logiweb是累积的，仍然可能有作者不再愿意为某篇旧论文的某个旧版本贡献磁盘空间的情况当上面的人B发布第9··· 91页时，该页将实际驻留在B的计算机上。然而，B可以删除第9··· 91页，这使得C然而，通过在Logiweb上发布，B隐含地将版权许可授予其他Logiweb服务器，以逐字复制该页面。特别地，人C当页面的最后一个副本消失时，页面将从Logiweb中消失。当一个页面消失时，它可能会开始雪崩，因为所有直接或间接引用该页面的页面都变得不完整。当浏览器加载页面时，它还必须加载所有直接或间接引用的页面，K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-77如果这些可传递引用的页面中的任何一个丢失，则浏览器应当报告该页面不存在。因此，当一个页面的最后一个副本消失时，它的所有依赖项也会随之消失。因此，当作者发布一个页面时，最好确保所有可传递引用页面的副本4数据结构Logiweb的主要数据结构是由符号组成的解析树，以及将方面与符号相关联的代码解析树定义了页面的结构，类似于MathML [11]中内容编码中的表达式树，并对应于OMDoc [10]中的树模型Codice以更类似数据库的结构表示页面的数学内容，该结构与Logiweb检查机器和编程语言接口良好。Logiweb codices以一种相当干净的形式包含数学语义，而不是OMDoc（[10]，p.65）的更语法化的数据库结构。4.1符号定义f（x）=stecto为x2−1。x2−1在上面第9··· 91页定义了f（x）对于Logiweb，f是一个“Logiweb符号”。Logiweb符号是一对自然数，r，i，r是符号主页的引用，i是标识该页面中符号的自然数。我们将把r和i分别称为r，i的“引用”和“索引”。作为一个例子，f可以是109···91，1 π。4.2解析树每个Logiweb页面都包含一个参考书目、一个“解析树”和一个“arity table”。解析树有以下语法（类似于Lisp S表达式）：解析树：：=符号{，解析树}解析通常，解析树是解析器的输出，它将人类可读的格式转换为机器友好的格式。在Logiweb中，方法是相反的：解析树是存储在系统中的实体，人类可读的形式是从它派生出来的。78K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-++元数表将元数分配给页面的符号，也就是说，一个引用为r的页面定义了形式为r，i，r的符号的元数。LogiWeb强制所有的解析树都具有形式p1，p2，p1， p 1 。，parity（s）其中arity（s）表示s的arity。4.3方面ToLogiweb，f（x）=stecx2−1是以下的简写：定义（Value，f（x），x2−1）这表明f（x）的“值方面”是x 2 −1。一般来说，定义（x，y，z）定义y的x方面。作为另一个例子，定义（TE X，f（x），小f·左括号·x·右括号）定义了f（x）的对于Logiweb浏览器来说，f（x）是一个解析树，⟨⟨9···91,1⟩,x⟩TE X方面告诉浏览器如何在TE X中呈现f（x）其他方面可以告诉如何在例如MathML。通过省略f（x）的TEX定义，简化了示例中的问题。一般来说，引入新符号的页面需要一个附录，定义新符号在各种格式中的外观，比如优先级和符号的关联性。对于Logiweb，都是规则P0：（x）x+0 =x，理论S：P0<$PJ<$Transitivity，S+引理L2.3.1：x=x+ 0，以及L2.3.1的证明：···定义（规则，P0，（x）x +0 = x），定义（理论，S，P0<$P J <$Transitivity），定义（引理a，L 2。3.1，S+S定义：x=x+0），和d定义（证明，L 2.3.1，···）保留部分。Above，x表示理论中可证明的引理X.K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-79+函数f（x）由y[f（x）=stecx2−1]定义。[RuleP0：（x）x+0 =x][RulePJ：（x，y）x+yJ=（x+y）J][Rule传递性：（x，y，z）x=y<$x=z<$y=z][理论yS+：P 0<$P<$Transitivity][S+lemmaL2.3.1：x=x+0]J形式上，一个方面是一个符号。为了让像Value这样的构造表示Value方面，必须将Value的Message方面定义为代表Value方面的符号。作为另一个例子，还必须将Message构造的Message方面安排为表示Message方面的符号。如何做到这一点是解释在第9节，其中涵盖了自举。4.4抄本Logiweb浏览器维护一个“Logiweb codex”，它存储浏览器遇到的定义。形式上，codex是一个稀疏的五维数组C（c.f.第B.6节），C[pr][sr][si][ar][ai]表示符号的方位，符号的方位，如第20p r页所定义。例如，当浏览器加载9··· 91（B然后它在法典中指出，第9··· 91页定义了符号的价值方面，1999···91，1通过解析树定义（Value，f（x），x2−1）。当浏览器加载时9··· 94（B然后它注意到，第9···94页将符号109··· 94， 1的规则方面定义为定义（规则，P0，（x）x+ 0 =x），符号109···94， 2的规则方面也类似，1994年3月3日。 然后指出，符号99···94， 4的理论方面是定义（理论，S，P0<$PJ）传递性和1999···94， 5的引理方面是定义（引理，L 2.3.1，x =x+ 0。当浏览器加载时80K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-函数f（x）由y[f（x）=stecx2−1]定义。[定义（TE X，f（x），小f·左括号·x·右括号]我们有[g（10）= 99]。[定义（TE X，g（x），小g·左括号·x·右括号][L2.3.1的证明：L1：P0L2：P0x+0 =x;x+0 + 0 =x+0;L3：及物性DL2D L2 x+0 =x+0;L4：及物性DL1D L3 x=x+0]9··· 95（C它指出，第9···95页将符号109··· 94， 5的Proof方面定义为冒号之后的解析树。5独立Logiweb是一种允许独立作者发布相互依赖的页面的媒介。本节给出两个例子，说明法典的结构如何允许独立性和相互依存性共存。5.1记法自由如前所述，第9··· 91页遗漏了f（x）的TEX方面的定义。一个更完整的页面应该是：9··· 91（B如果C想使用f（x），但为了其他目的保留了f，那么C可以将f重命名为g，如下所示：9··· 92（C上图中，g（x）是符号9···91， 1的伪装。上面的页面可能会混淆人类读者，因为C懒得评论g（x）在他的页面上与f（x）和B的页面相同但浏览器只会注意到第9··· 91页和第9··· 92页将第9···91页和第9···92页的T E X方面定义为两个不同的事物，并且将在分别显示第9···91页和第9·· 92页时使用第9··· 91页和第9··· 92页的TEK. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-81因此，B调用函数f（x）的符号自由并不限制C将其重命名为g（x）的符号自由。这一点很重要，因为世界范围内关于符号的协议将要求所有数学家为他们的概念使用不合理的长名称。Logiweb在符号上强制全球一致，因为每个符号都包含一个页面引用，RIPEMD-160强制该页面引用是全球唯一的，但与人类可读的符号表达无关。5.2替代证明第4.4节给出了一个例子，其中第r = 9···95页定义了符号s = 9 ··· 94，1的方面a=“证明”。一般来说，代码是一种关联结构，它将值与参考符号体三元组（reference-symbol-aspect triples）关联起来。不同的页面可以定义符号的证明方面94， 1不同，因此，法典可以应付不同作者为同一引理发表不同证明的情况。6宏为了保持de Bruijn因子[5]较低，Logiweb包括一个简单但功能强大的宏工具。宏功能允许作者以吸引人类读者的风格编写页面，但仍然可以将其宏化为更机器可理解的形式。6.1宏定义Logiweb有一个默认的宏工具。就像Logiweb中的其他东西一样，页面可以通过指定替代选项来覆盖默认值。作为使用的一个例子，考虑以下定义：定义（Macro，h（x），h（x）→<$x2−1）上面的定义表明h（x）是x2−1的简写。f（10）和h（10）的值都是99，但如果h（10）出现在证明中，那么在证明检查之前，它会扩展到102− 1。作为一个更复杂的例子，假设x：：y表示x和y的对，而x-y表示空元组。此外，假设x，y和x，y分别是一元和二元结构，并考虑以下宏定义：定义（Macro，x，（u）（v）u，v→u： ：v>x→x：：）该定义是，x必须由x，v，v如果解析树x在其根中有一个逗号运算符，则应简化为x：：逗号82K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-否则，请执行以下操作。举个例子，1，2，3（其中逗号是右关联的）将宏缩减为1：：2：：3：：，如下所示：1，2，31：：2：：13→1：：2：：3：：游戏作为又一个例子，定义e（Macro， x=y，（z）x=y=z→¨）的结果是，例如，x=y=z）1+2+3+4= 3+3+4 = 6+4 = 10宏简化为1 + 2+3+4 = 3+3+4 3+3 + 4 = 6+4 6+4 = 10”（《礼记》12：16）。使用macroreduction的操作符。在上面的宏定义中，x和y是元变量，因为它们作为被定义的符号的参数出现，z是元变量，因为它被元量化器量化一个特别重要的宏读取定义（Macro，（x），（x）→？x它说在证明检查之前应该从解析树中删除括号。6.2宏观定义宏工具允许语法的大量简化。首先，定义定义（宏， x=<$y，x=<$y→<$）允许定义（Macro，x，x→¨（y））作为作为另一个例子，定义（Macro，h（x），h（x）→<$h（x）=？x2−1x2−1）定义x=stecy。x=stecy=<$De fine（Value，x，y）K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-836.3Metalogic的宏下面的宏定义定义了几个用于在2.3节中引入规则、理论、引理和证明的结构：规则x：y=？De finne（规则，x，y）或yx：y=？De finne（理论y，x，y）xLemmay：z=<$Define（Lemma，y， x）Proofx：y=<$Definee（Proof，x，y）结构xxxz表示mz是理论的一部分X. 元连接词的完整列表见8.5节。7编程语言像大多数其他证明系统一样，Logiweb包含一种编程语言。Logiweb的编程语言允许表达边条件，证明策略，复杂的宏，复杂的渲染方案和许多其他东西。像Nuprl [4]和Isabelle [13，14]一样，Logiweb使用基于lambda演算的编程语言。Logiweb使用了一个非常简单的无类型的lambda演算。选择简单性是为了使Logiweb易于推理，并且易于实现，而（较小的）代价是编程必须从相当低的级别开始所选择的编程语言是映射理论的编程语言[2，7，15，17]，并使用常数nil和构造ifnil（x，y，z）扩展了λ-演算[3]。 ifnil（x，y，z）构造具有以下性质：函数λ x的值域。如果nil（x，y，z）equals{y，z，n}（其中n=stecapply（S，S），S=stecλ x。apply（x，x））。因此，编程语言包括函数其值域恰好有三个元素，这在纯λ-演算中是不可能的。这个属性允许使用“quartum non datur”规则[2，7，15，17]来推理程序除了y、z和m之外的其他值此外，ifnil的存在允许编程语言有非常简单的，非平凡的模型，比纯λ演算的模型更语义化，更少语法化。7.1评价Logiweb的编程语言提供了四个基本结构：λx.y，apply（x，y）、ifnil（x，y，z）和nil。定义f（x）=stecx2−1anddclaimf（10）= 100的前提是xy，x-y，x=y，而数是从这四个结构中定义的[8]）。84K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-当浏览器验证一个声明时，它使用正常顺序归约[1]根据以下归约规则来ifnil（nil，y，z）→yifnil（λu.v，y，z）→zapply（nil，z）→nil apply（λx.y，z）→nily|x：= z以上四个以外的术语通过在法典中查找它们的价值方面并使用它来减少。如果一个项没有值方面，它就归为nil。如果一项索赔减少到零，则该索赔被接受，如果减少到形式为λx.y.Logiweb编程语言也用于验证边条件时：When enchecinga pr oofforme. G.（（x，y）（<$free（x，y）<$x：y∈x））u：如上所述，Logiweb编程语言也用于系统中的许多其他情况。7.2地图理论Map TheoryLogiweb最初是为了支持地图理论而开发的[2，7，15，17]。映射理论是上面用量化器扩展的归约系统，具有ZFC集合论的力量。然而，Logiweb已经脱离了地图理论，所以Logiweb同样很好地支持所有理论。一个例外是，由于Logiweb使用嵌入在Map Theory中的编程语言作为用户编程语言，Map Theory特别适合于对Logiweb进行推理，即，作为系统的元理论。8验证任何证明系统的一个主要特征是系统能够验证呈现给它的数学的正确性。Logiweb采取的方法是每个作者可以提出“声明”，然后由Logiweb来验证声明。一个页面是正确的，如果它的声明是正确的。一页没有任何声明是微不足道的正确。以下几页描述了各种类型的权利要求和表达这些权利要求的各种工具。K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-858.1页码如前所述，一个法典将值与参考符号体三元组相一个，一个，一个。有时，需要定义页面的各个方面，而不是符号的各个方面。例如，页面的声明与整个页面相关联。为了解决这个问题，同时保持抄本的一致性，约定是用一个id等于0的符号p，0表示页面p。id等于零的符号将被称为“页面符号”。Logiweb强制所有页面符号的arity为零。Logiweb提供了构造其中r是Self出现的页面的引用。8.2简单的结论下面的宏观定义定义了简单声明的结构[x]=-De finne（Test，Self，x）因此， 一个claimlike[f（10）=99]对于定义（测试，自我，f（10）= 99）出于这个原因，在页面上提出的声明将进入codex，当用户想要验证页面时，浏览器可以访问并执行codex中的声明。8.3多个定义如果一个页面包含同一符号的同一方面的多个定义，那么浏览器会收集所有定义的列表，然后从所有定义中合成一个定义。默认情况下，定义是从一个列表中合成的，如下所示：如果所有定义都相同，则使用其中一个，否则法典存储一个值，表明定义是错误的。然而，主张方面的处理是不同的，因为所有的定义都被连接成一个连接词。因此，可以在一个页面上提出多个索赔8.4索赔总额除了简单的类似于k[f（10）=99]之外，一个页面也可以通过如下定义来实现一个非一般性的声明：定义（索赔，自我，T）86K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-如果一个页面使用类似上面的定义进行整体声明，那么如果apply（T，Self）的值为nil，则该页面被认为是正确的。如果T实施例，例如[12，16]，那么该页面声称是开阳正确。 这样一个术语T很可能使用大量的定义来定义，可能分散在许多页面上，并且必须用Logiweb的编程语言来表达。以这种方式将其他系统（如Mizar）包含在Logiweb中的好处之一是，系统的每个版本都被冻结并且页面的正确性将总是与系统的一个特定版本相关。因此，每个正确性声明将是恒定的，即使所讨论的系统正在开发中。如果一个页面没有总体声明（或者总体声明是错误的），浏览器应该使用默认声明来检查页面，默认声明是所有简单声明的值都应该为零，所有证明都应该是正确的，没有定义应该被标记为错误。8.5Metalogic默认的整体声明承认以下规则、理论、引理和证明的语法：规则：：=规则|反倾销规则|（Ter m）规则|TermTheory：：=/T e rm Theory|理论理论|规则Lemma：：=Or y yyTermProof：：= Proof D Proof|证明Term|术语：证明|证明;证明|规则上面，一个术语表示任何不包含任何元结构（xy，xy，and dsone）的解析树。如果x是可预测的，则y是可预测的。x表示如果x将s赋值为“真“，则y是可逼近的（x）y表示y对所有项成立X.作为规则陈述的术语表示公理。/nx声称x在它所发生的理论中是不可证明的，这允许谈论理论的一致性。x≠y表示包含理论x和y的所有规则的理论。 一个规则被当作一个历史记录来记录，并不代表它是一个电子规则。xy表示y是理论x的定理的引理。xDy表示应用于证明x和y的结论的元肯定前件。 x y表示从证明x得出y项。x：y局部引入x作为证明y的结论的简写。x;y与y有相同的结论，并允许y使用x的结论，就好像它是公理一样。作为证明陈述的规则以规则本身作为其结论，并要求规则属于理论K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-87市.我们9自举如前所述，Logiweb操作员对其用户完全享有符号自由。虽然这非常方便，但它使开始的问题变得复杂。Logiweb在从已知的结构中定义新的结构方面具有很大的灵活性，但是如何才能从无到有地引入第一个结构呢？本节讨论这个自举问题。第9.2节解释了如何使用一个单一的“宣告”结构来引入所有预定义的结构9.1预定义符号形式为“0”、“1”的符号将被称为“预定义”符号。预定义的符号具有由自然数i固定的意义。对页面的引用总是正整数，并且解析树中所有符号的引用都指向Logiweb系统中存储的页面，因此预定义的符号不能出现在解析树中。然而，预定义的符号可以出现在法典中9.2公告假设small-a表示一个解析树，其根符号的id等于小“a”的ASCII码ID等于97）。假设small-b、small-c等具有类似的性质。进一步假设x·y是arity为2的右结合构造，End是arity为0的构造一份宣言，宣 告 （ apply （ x ， y ） ， small-a· small-p· small-p· small-l· small-y· End）定义构造apply（x，y）来表示函数应用。当Logiweb浏览器看到类似上面的定义时，它会在codex中指出，给定的页面将apply的Value方面定义为0，i，其中i是标识功能应用程序的id。宣告构造Proclaim（x，y）允许将任意的符号附加到任意的、预定义的概念上。例如，apply（x，y）、Value、Message和Define（x，y，z）由声明定义公告结构甚至允许定义新的公告结构。88K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-9.3基本页面参考书目为空的页面将被称为“基页”。如果r是一个基本页面的引用，那么浏览器应该把r，1看作一个声明结构。因此，在Logiweb上引导的过程如下：发布一个基本页面。使用基本页面的宣告结构将符号与所有其他预定义的结构相关联。然后用这些符号来做定义、测试、规则、理论、引理、证明等等。9.4系统提供的方面用户可以定义符号的各个方面，但有几个方面是由Logiweb浏览器提供的：每个页面最终都存储为“向量”，即字节列表。 当浏览器用引用r加载页面，它将页面的矢量存储为页面符号的矢量方面。换句话说，浏览器将r每个页面都包含一个参考书目，它是一个参考文献列表，以及一个解析树;浏览器将它们分别存储为页面符号的Bibliography和Parsetree方面。如果页面是基本页面（即如果页面的参考书目为空），则将符号编号1的编码方面设置为“0”，其中“0”，“i”是识别公告结构的预定义符号。每一页都定义了每个符号的重要性对于具有非零arity的每个符号当浏览器加载一个页面时，它也会加载所有传递引用的页面，如果它们还没有在法典中。然而，浏览器也构造了一个仅包含可传递引用页面的codex子集，并将该子集存储为页面符号的Cache方面。最后，当浏览器加载了一个页面时，它将与该页面相关联的部分代码添加到上面的子集中，以获得该页面的“本地代码”（与给定页面相关的部分代码）。然后，它将本地代码存储为页面符号的值方面。Logiweb评估器只能访问符号的值方面，但可以通过此机制访问与给定页面相关的所有法典。因此，Self宏总是扩展为值为本地codex的内容。K. Grue / Electronic Notes in Theoretical Computer Science 93（2004）70-89ALogiweb协议层0A.1平台在硬件层面，Logiweb由许多主机支持，这些主机通过许多主机网络互连。举个例子，如果Logiweb运行在许多通过Internet互连的PC上承载Logiweb的计算机和网络不需要专门用于相反，托管Logiweb的计算机和网络通常也会托管其他系统。在软件级别，Logiweb服务器或Logi-web浏览器的每个实现都由主机操作系统（例如Linux）、主机编程语言（实现语言）和多个主机协议（例如，TCP/IP）。A.2层Logiweb协议有三层。第0层涉及字节的存储、检索和传输。Layer 0定义Logiweb服务器的行为。第1层涉及将页面解包为codice，以及页面的检查和呈现Layer 1定义了Logiweb浏览器的最小第1层以上的层由用户定义，并且不在Logiweb协议的范围内。本章介绍协议的第0层。A.3位和字节编号约定在一个字节内，我们将权重为2i的位称为位号i。因此，最低和最高有效位分别是位号0和7。在TCP/IP中，第0位首先传输，第7位最后传输。在字节向量中，我们将第一个字节称为字节数0。在TCP/IP协议中，字节数0是传输的第一个字节。当在本文中写入字节向量时，字节号0被写在最左边。当在本文中将字节写为8位时，位号0写在最左边，这与正常实践相反。这样做是为了避免字节序列中的位编号问题