OOPS：一个用于教育环境的S5n证明器

理论计算机科学电子笔记262（2010）249-261www.elsevier.com/locate/entcsOOPS：一个用于教育环境的S5n证明器Gert van Valkenhoef1，2荷兰格罗宁根大学商业与信息通信技术系P.O. Box 800，9700 AV，格罗宁根，荷兰Elske van der Vaart3格罗宁根大学人工智能系P.O. Box 407，9700 AK，格罗宁根，荷兰格罗宁根大学理论生物学小组P.O. Box 14，9750 AA，Haren，荷兰Rineke Verbrugge4格罗宁根大学人工智能系P.O. Box 407，9700 AK，格罗宁根，荷兰摘要我们提出OOPS，一个开源的，跨平台的，易于运行的Tableau证明器的S5n. OOPS旨在进行模态逻辑的教育。因此，它有几个特点，使洞察其内部工作。具体来说，OOPS允许可视化表格，并可以为公式生成反模型，无法证明。此外，OOPS图形用户界面（GUI）增加了易用性和集成的通用脚本语言（Lua）用于提供与OOPS画面生成器。关键词：系统描述，模态逻辑，认知逻辑，S5n，Tableau方法，教育，可视化1介绍本文介绍了一个面向对象的S-5n探测器OOPS-5.它是一个基于表格的定理证明器，旨在进行满足性检查，专门设计用于课堂环境。虽然没有高度优化的效率高1通讯作者。2电子邮件：g.h.m.van. rug.nl3电子邮件地址：elskevdv@ai.rug.nl4电子邮件：rineke@ai.rug.nl5http://wiki.github.com/gertvv/oops1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.018250G. van Valkenhoef等理论计算机科学电子笔记262（2010）249无论是像MSPASS [12]和FaCT [11]这样的证明器，还是像LoTReC [7]和TableauReader [1]这样的高度可扩展的证明器，我们都相信OOPS提供了一个独特的功能组合，使其特别适合教育目的。首先，OOPS操作程序支持S5n，这种逻辑通常用于对人类推理过程进行建模.据我们所知，目前还没有其他的定理证明器可以做到这一点。此外，OOPS能够可视化其tableau证明，并生成反模型的公式是假的。这两个属性对于教育证明工具非常有用，并且至少有两个其他系统共享它们：LoTReC可以显示其tableau树，而Logics [10]可以在微积分中打印它的导数OOPS与LoTReC以及MSPASS的另一个共同点是它的免费和方便的分发，但很少有其他定理证明器。OOPS被打包为一个ZIP文件，其中包括所有的依赖关系，一旦提取，可以简单地运行双击生成的oops.jar文件。对于任何操作系统都是如此，只要Java VM可用。相比之下，Tableau SDK必须从源代码构建，FaCT SDK仅为Linux和Windows提供二进制文件，否则需要Lisp，而Logics SDK不是开源的，并且由于过时的依赖关系而难以安装OOPS在教育用途上特别有吸引力的一个重要特性是图形用户界面（GUI）。虽然简单，但其GUI允许学生以简单直观的格式输入公式，或保存和加载文件。LoTReC、MSPASS和逻辑控制器也支持基于GUI的访问。OOPS在我们的实验中，大多数涉及定理证明的学生项目都是模拟谜语或游戏情境的尝试。 这要求学生能够建立和扩展理论- 在必要时使用循环和条件句。许多证明工具，如逻辑证明工具，或用于此目的的自定义脚本语言。相反，OOPS集成了现有的Lua6脚本语言。Lua可以用来调用OOPS总之，我们的贡献是一个证明系统OOPS，旨在支持逻辑教育，特别是多智能体推理。为此，OOPS提供了一个S5n的tableau prover，能够可视化其tableau proof和反模型，以证明公式是假的。此外，OOPS是平台独立的，易于安装。最后，OOPS提供了一个图形用户界面（GUI）和一个集成的脚本语言（Lua），可以与证明器进行简单而强大的交互。在本文的其余部分，我们首先介绍了OOPS的技术描述，包括它的证明系统，它的形式属性，它在Java中的实现，以及细节它的输入语言（第2节）。 其次是更详细的描述OOPS最后，我们讨论了目前的局限性和未来的工作（第5节）。6http://www.lua.org/G. van Valkenhoef等理论计算机科学电子笔记262（2010）249251∈·∈ ¬∈2技术说明在本节中，我们将首先简要描述OOPS中使用的tableau方法，并总结系统的形式属性（可靠性，完整性，复杂性）。然后，我们解释了如何在Java中实现Tableau系统。最后，我们描述了由OOPS提供的模态公式的输入语言。2.1OOPS表格S5n 的 OOPStableau 系 统 是 证 明 系 统 ELtap[4 ， 3] 的 Java [8] 实 现[ 5 ][2 ][3][4][ 5 ][ 5][6][7][8][9][9][10][11][12] [9]提供了一个很好的审查表方法的模态逻辑。在这里，我们总结了如何在OOPS中形式化的tableaux。完整描述见[14]。当我们构建一个表时，我们这样做的目的是创建一个克里普克模型，其中一个公式满足。这是通过假设是真的，然后系统地计算出这个假设的含义来实现的。具体来说，OOPS生成一个分支集合，每个分支代表解决这些含义的替代方法。分支B由若干节点组成。一个节点γ是一个公式和一个标签σ的组合。 在克里普克模型中，标签是为一个正在构建的世界系统选择的名称。 通过将规则应用于分支上的现有节点来创建和扩展分支。规则R包括：• 一个前置条件pre（R），写在一个水平条的上方，这是一个包含变量的节点;• 后置条件post（R），写在水平条下面，是包含变量的节点列表。有两种类型的后置条件：Linear：向当前分支添加节点，从上到下写;分支：创建一些新的分支，从左到右写，用竖线分隔。• 零个或多个约束，这些约束限制变量可能采用的值OOPS采用的规则见表1。规则R适用于分支B，如果存在匹配pre（R）的节点γ B，使得没有违反约束并且R先前没有应用于γ。在模态规则的情况下，在匹配了前提条件pre（R）之后，我们可能需要创建一个新的世界（添加标签部分）或匹配现有的世界（标签）。 在第一种情况下，我们创建一个唯一标识的标签部分，通过 将公式编码为有效标签部分的函数在后一种情况下，后置条件将包含一个变量作为其中一个标签部分的占位符。这样的后置条件必须应用于其标签匹配的所有标签一个分支B是闭的，如果有一个标签σ和一个公式σ，使得（σ，σ）B和（σ，）B. 分支B是开放的，如果它没有关闭，没有更多的规则可以适用于它。因此，开放分支对应于成功地尝试满足k，而闭合分支对应于失败地尝试满足k。具体地说，对于一个开分支B，标签决定了世界的集合，··252G. van Valkenhoef等理论计算机科学电子笔记262（2010）249双重否定规则合取¬¬σ¬¬ϕσ ϕ∧∧∧∨规则σ ϕ∧ψσ ϕσ ψσ<$（）σ¬ϕσ¬ψ选言规则∨∧∨∨可能性MQMQ规则（其中i=j）σ。ki<$Qj<$σ。基岛¬ϕσ.kiQj<$σ.ki. 吉可能性MQMQ规则σ.ki<$Qi<$σ. ¬ϕσ.kiQi<$σ. 伊苏基本必需品KQKQ规则（其中i=j）σ.kiQj<$σ.ki.hj<$σ。ki基本必需品KQKQ规则σ.kiQiσ.hiσ.ki<$Qi<$σ.hi <$特殊需要TQTQ规则（其中i=j）σ.kiQjσ.kiσ。ki<$Qj<$σ.ki<$特殊需要RQRQ规则σ.kiQiσ表1σ.ki<$Qiσ<$Tableau扩展规则（有关OOPS如何应用这些规则的说明，请参见第2.2Kripke模型中的可及性关系。对于每一个标签，为该标签给出的一组公式决定了相σ<$（）σ<$σ<$σσ ϕ σ ψϕ∨ψG. van Valkenhoef等理论计算机科学电子笔记262（2010）249253应世界中的估值在Kripke模型中。 如果所有分支都是关闭的，则表示为关闭，否则它是开放的现在，对于任何证明系统，重要的是它的证明完全符合逻辑的语义OOPS使用的证明系统已被证明，254G. van Valkenhoef等理论计算机科学电子笔记262（2010）249对于S5n来说，这是合理且完整的[14]。此外，在同一工作中，实现（第2.2节）被证明与形式描述相对应的证明方法。 不幸的是，这项工作也表明，使用的算法， 在最坏的情况下，OOPS需要指数时间，而S5n的可满足性已知是PSPACE-complete [9]。然而，我们相信，出于教育目的，OOPS提供的功能（见第3节）很容易弥补这一缺陷。此外，这些功能的实现不依赖于所使用的特定证明算法。 因此，作为未来的工作，目前的算法可能会被替换为一个是在PSPACE。2.2执行为了确保表1当一个节点被添加到当前分支时，我们尝试匹配每个可能的规则到该节点。产生的匹配被放置在匹配队列中。 现在，基本必要性规则（表1）提出了一个特殊的问题：后置条件可能适用于尚未生成的标签。为了解决这个问题，这些规则的部分匹配的后置条件被存储在必需列表中。每当生成新标签时，此列表中与新标签的任何匹配都将添加到匹配队列中。这些数据结构是特定于分支的，即，当创建新分支时，它接收当前匹配队列和必需品列表的副本出于效率的原因，匹配队列是一个优先级队列，可以为规则指定一个数字优先级值，该值指定匹配应用于tableau的顺序。通过这种方式，我们可以确定尽快关闭分支机构的策略。例如，在尝试执行任何其他规则之前，最好执行所有可能的非分支命题规则这些规则以这样一种方式实现，即它们可以很容易地被不同的规则。 此外，Tableau生成器允许生成过程 被监控这使得诸如tableau可视化和反模型构造等特性的解耦实现成为可能（参见第3节）。2.3输入语言OOPS为使用Java的SableCC [6]编译器生成器实现的公式使用了一种输入语言。命题以字符串和数字的形式输入，以字符串开头。代理身份由自然数表示。OOPS使用广泛理解的fix符号表示逻辑公式。表2显示了不同逻辑运算符的OOPS等价物，以及它们的优先级;数字越小，绑定越强除此之外，该语言允许输入变量作为（子）公式或代理身份的占位符。这在规则的定义中很有用，并允许创建可以以不同方式实例化的模板公式，通过替换。变量是由字符和数字组成的字符串，以字符串开头。G. van Valkenhoef等理论计算机科学电子笔记262（2010）249255结缔¬∧∨→↔QIQIOOPS符号˜&|>=#i% i优先1234411表2OOPS连接器。3功能在本节中，我们强调了OOPS的一些功能，我们认为这些功能在教育环境中很重要。尽管其他系统可能会共享一些OOPS3.1集成脚本为了使定理证明器真正有用，在给定输入公式的情况下，能够回答“真”或“假”是不够的。相反，我们的经验表明，学生需要制定和扩展理论。通过手工编辑一个大的公式来完成这一点很快就会变得难以管理。 此外，我们希望有一个强大的工具箱来帮助我们制定更大的理论。这个工具箱应该包括一般的编程结构，如循环和条件。其他一些工具，如Logics工具，提供了用于此目的的自定义脚本语言。这种方法的优点是语言可以专门针对证明器的常见用法进行定制。 然而，缺点是开发自定义语言的成本很高。因此，最终的语言很可能缺乏表达能力。 此外，用户必须学习一种语言，该语言在证明器之外没有应用，并且对于该语言的支持（即，文档、用户社区和bug修复）可能受到限制。为了解决这些问题，OOPS集成了通用脚本语言Lua。Lua被专门设计成一种嵌入式语言，广泛用作扩展语言和编写的库的前端。在其他语言中。 因此，Lua使我们能够定义一个量身定制的环境满足定理证明的需要，同时避免了与实现定制语言相关的问题。 参见[13]，了解编程的良好介绍在Lua。目前，OOPS上面概述了我们将OOPS与Lua集成的原因。现在我们简单描述一下OOPS是如何通过Lua接口使用的。所有OOPS方法都封装在oops命名空间中。 通过Lua与OOPS交互的基础是理论概念。简单地说，理论就是公式的集合。下面的示例代码创建了一个理论，并向其中添加了一个公式th = oops。理论（）th：add（“# _1 p”）我们定义了一些关于理论的操作：一致性的检查，理论中公式的可证明性和理论中公式的可满足性256G. van Valkenhoef等理论计算机科学电子笔记262（2010）249∨print（th：consistent（））−−trueprint（th：probable（“# _2第一名p”））−−印刷错误（th： 可满足 （“~# _2p”））−−true其中--开始一个注释，这里用来表示print语句产生的输出。现在，为了帮助理论的构建，我们允许明确地创建公式，在此基础上我们定义了替换运算举例来说日=哎呀理论（）F=哎呀公式（“# _AV”）为i = 1，4，1d0th：add（f：substitute（{V = “p | q" } ,{A=（i））端print（th）其表示代理1、 2、 3和4结果输出为：[#4 （p|q）， 第三名（p|q）， 第一名（p|q）， 第二名（p| q) ]这就完成了我们对OOPS如何从Lua调用的描述。 必须指出的是，Lua是一种非常强大和完整的语言，比上述例子所建议的要好。例如，与用户的命令行交互可以通过Lua轻松实现3.2图形用户界面如上所述，Lua为OOPS提供了一个方便的脚本接口。然而，现代计算机用户并不期望从命令行运行应用程序.即使他们习惯了这个概念，它也不总是最方便的互动方法。因此，OOPS包括一个非常简单的图形用户界面（GUI），其中可以显示，编辑和执行脚本（图1）。此外，脚本可以从文件中加载并保存到文件中。对于那些喜欢使用外部编辑器的人（例如， 有许多编辑器可以提供语法高亮显示功能对于Lua），一个组合键从文件系统重新加载一个修改过的文件。该应用程序由两个面板组成：顶部面板显示当前脚本，底部面板显示输出。尽管最小化了，但GUI极大地增强了OOPS的使用便利性。首先，脚本和输出显示在一个地方，便于交叉引用。其次，脚本通过单个组合键（或从菜单调用）运行。最后，加载、保存和刷新功能使用户可以自由地使用集成编辑器或外部编辑器，同样方便。3.3免费和方便的配送正如我们在第1节中所指出的，大多数当前的证明工具都存在与平台依赖性、老化依赖性、缺乏维护或难以安装程序相关的问题。OOPS以几种方式解决这些问题。首先，OOPS是用纯Java实现的，这意味着OOPS将在任何有Java虚拟机可用的操作系统上运行。对于大多数运营商来说，G. van Valkenhoef等理论计算机科学电子笔记262（2010）249257图1. OOPS图形用户界面。系统目前可用。 其次，OOPS是作为一个ZIP文件分发的，其中包括所有的依赖关系。无需安装，只需提取ZIP文件并双击生成的oops.jar文件。因此，OOPS是平台无关的，易于运行，除了Java VM和所提供的内容之外没有任何依赖性在OOPS分布中。持续维护的问题更难解决。为了确保OOPS可以在未来被任何希望这样做的人使用和扩展，我们在GNU通用公共许可证（GPL）下提供了完整的源代码。我们希望其他人将为OOPS贡献扩展。3.4表格可视化当一个学生学习模态逻辑时，证明者往往会给出令人惊讶的结果。他或她在构建理论时可能会遇到不希望的结果，并希望能够通过检查证明过程来“调试”理论。此外，检查生成的tableaux可以增强对tableau方法和模态逻辑语义的理解。为了支持这一点，OOPS包括一个可视化模块，用于标记tableaux。 图2显示了这种可视化的示例。画面被画成一棵树。在树中，节点按添加顺序编号（每行最左边）。在节点编号之后，将显示标签，然后是公式。最后，给出导致创建特定节点的规则以及规则匹配的节点编号。可视化是作为Tableau生成器上的观察者实现的（参见第2.2节）。生成图2的Lua代码如下（注意命令行输出将为true）：哎呀.a ttachTableauVisualizer（）下一页print（oops . 理论（）： 可证明的（“（# _1 p|#_1~p）>#_1（p |~ p）”）7http://github.com/gertvv/oops258G. van Valkenhoef等理论计算机科学电子笔记262（2010）249¬∨ ¬ →∨ ¬图2. 通过尝试满足k，检查k的可证明性的画面的可视化，其中k=（（Q1pQ1p）第一季度（p（p））。 在这种情况下，该表是封闭的（即，可证明的），如每个分支下的=（m，n）所指示的，其中m和n指示两个矛盾的找到了公式3.5反模型的可视化除了能够查看工作表之外，能够检查工作表所对应的模型可能会有所帮助。 如果tableau是开放的，生成的模型通常会更有洞察力，因为它不包含任何冗余信息。与Tableau可视化的情况一样，（反）模型的可视化可以增强对模态逻辑语义的理解图3是由以下Lua代码生成的（注意命令行输出将为false）：哎呀.attachModelConstructor（）下一页print（oops .理论（）：可证明的（“# _1p | # _1~p”））哎呀 show Model（）正如读者所注意到的，模型可视化的调用与Tableau可视化不同。这是因为我们将模型视为实体本身。实际上，如果上次调用tableau generator导致打开tableau，则调用oops.getModel（）可用于检索最近构造的模型。Lua的print函数将输出模型的文本表示。然而，进一步的编程操作和模型检查是未来的工作。图3. 一个反模型的可视化，其中，Q=（Q1p<$Q1<$p）。 The ‘main’ world is indicated inG. van Valkenhoef等理论计算机科学电子笔记262（2010）249259−−−−−−−−−−−−4例如为了说明OOPS的教育潜力，我们提出了一个示例，该示例模拟了我们过去在格罗宁根大学人工智能系分配给多智能体系统学生的练习。 我们展示了OOPS 我们的例子涉及一个简化版的有两个聪明的人，阿伯拉尔（1）和埃洛伊丝（2）。大家都知道有三顶帽子：两顶红色的，一顶白色的。 国王戴上帽子两个聪明人的头上，谁也看不见自己的帽子， 可以看到对方的帽子（他们都知道这一点）。国王依次问他们是否知道自己头上帽子的颜色。第一个人，阿伯拉尔，说他不知道;第二个人，埃洛伊丝，说她知道。练习：找出Heloise帽子的颜色为了模拟这个问题，让我们定义命题r1为在这个例子的完整实现中，可以在线获得，8给出了一些效用函数conj（f1，f2）安全地给出两个公式的连接，knows（a1，f）给出公式Qa1f'，knows2（a1，a2，f）给出Qa1Qa2f. 最后，在理论 th 下 ， printAbelard （ th ） 和 printHeloise （ th ） 给 出 了 Abelard 和Heloise知识状态的信息输出.最初的情况可以通过简单地定义给定的基本事实来模拟。并指出阿伯拉尔和埃洛伊丝都知道这些事实足够的深度。当然，背景信息应该是常识，但这在纯S5n中是不可能的。 所以我们把知识赋予深度2，解决这个难题所需的最低水平Lua代码如下：每个人具有只一顶帽子oneHat= “（r1=~w1）&（r2）=~w2）”There reI s只一白帽子oneWhite =“（w1 >r2）（w2 >r1）”&阿伯拉尔可以看到埃洛伊丝的帽子阿贝拉尔湖 =“#_1W2 | # _1r2“海洛伊丝可以看到阿伯拉尔帽子海卢瓦塞=“#_2W1 | # _2 r1 "背景知识：background = co n j（co n j（oneHat，oneWhite），conj（abelardSees，h e loiseSees））添加背景知识和智者th = oops。理论（）th：添加（背景）th：add（knows（“1”，background））th：add（knows（“2”，background））8http://cloud.github.com/downloads/gertvv/oops/hats.lua−−260G. van Valkenhoef等理论计算机科学电子笔记262（2010）249−−−−−图4.反模型Heloise知道她自己的帽子的颜色在“智者”难题的初始情况。 与Abelard知道他的帽子颜色的反模型几乎是相同的，除了世界之间的关系是针对特工1（Abelard）的，而不是特工2（Heloise）。th：添加（knows2（“2”，“1”，背景））th：add（knows2（“1”，“2”，背景））我们可以使用以下语句来评估代理在初始情况下的知识：使确定我们可以显示的counter model哎呀.attachModelConstructor（）下一页print（“Initial Situation：“）printAbelard（th）打印Heloise（ th）哎呀 show Model（）Heloise知道自己帽子颜色的反模型如图4所示。控制台输出如下：I n i t i a l情况：阿伯拉尔在拼图中，阿伯拉尔被问到是否知道自己帽子的颜色，他没有Heloise现在可以推导出她的帽子的颜色。我们通过让Heloise知道Abelard不知道他的帽子的颜色来模拟这个声明后阿伯拉尔宣布他不知道：abelardKnows =“# _1W1 | # _1r1“th：add（oops . 公式（“# _2~F”）：替换为（{F =abelardKnows}，{}））printt（“AfterAbelard哎呀howModel（）printHeloise（ th）print（“一致：“..tostring（th：consistent（）输出如下所示后阿伯拉尔公告：阿伯拉尔不海洛伊丝知道他/她的帽子是红色的一致：正确显然，阿伯拉尔仍然由上述代码生成的计数器模型几乎是G. van Valkenhoef等理论计算机科学电子笔记262（2010）249261与图4中所示的相同，因此没有单独示出。这个例子演示了可以用OOPS设计的赋值类型。它给学生使用定理证明器的经验，并让他们用不同的假设进行实验，提供对熟悉的谜语背后的形式逻辑的洞察力。由于OOPS5结论和进一步工作在本文中，我们提出了OOPS，一个跨平台，易于安装和开源的Tableau证明器的S5n。OOPS为用户提供了一个图形用户界面，一个集成的脚本语言，tableau可视化和反模型生成。我们相信这些功能使OOPS比其他类似系统更适合教育用途。鉴于此，我们现在确定OOPS进一步工作的几个方向。首先，尽管目前的实现允许相对容易地实现新的规则集，但这需要扩展Java源代码并重新编译OOPS。为了解决这个问题，我们希望将规则集实现为Lua模块，并为几个逻辑提供这样的模块。Lua是专门设计的，可以很容易地实现特定领域的语言。这个功能可以用来提供公式输入语法与Lua的更直接的集成，使公式输入看起来像本地语言支持。Lua绑定总体上应该得到改进，但这需要作为一个教育工具从实际使用中得到进一步的投入。我们我也想实现一个算法，允许在PSPACE中生成S5ntableau，因为我们目前的实现可能需要指数级的空间。此外，我们希望有一套更完整的工具来与理论，公式和Kripke模型进行交互。例如，应该可以简化公式和理论。在Kripke模型的情况下，我们希望能够自己构建和修改模型，并执行模型检查和互模拟等操作。最后，GUI应该允许用户向Lua脚本提供键盘输入（通过引用[1] 阿巴特山口 和R. 理论计算机科学电子笔记231（2009），pp. 55比67[2] Beckert，B.和R. Gore，Free variable tableaux for propositional modal logics，Automated ReasoningWith Analytic Tableaux Related Methods1227（1997），pp.91比106[3] de Boer，M.，“Praktische Bewijzen in Public Announcement Logica,” Master’s thesis, University ofGroningen, Groningen, the Netherlands[4] deBoer，M.， KEtabl e auxforPublicAnnoun cementL ogi c，in：B. 杜宁-凯普利河 Verbrugge，editors，FAMAS'007，2007，pp. 56比69262G. van Valkenhoef等理论计算机科学电子笔记262（2010）249[5] 很合适，M。和R. Mendelsohn，[6] Gagnon，E'.，“SableCC，一个面向对象的嵌入式框架工作”，硕士论文，麦吉尔大学，蒙特利尔，魁北克，加拿大（1998年）。[7] 加斯盖岛，A. Herzig，D. Longin和M. Sahade，LoTReC：Logical Tableaux Research EngineeringCompanion，in：B.Beckert，editor，TABLEAUX 2005（2005），pp.318-322[8] Gosling，J.，B.乔伊，G。L. Steele和G. Bracha，[9] Halpern，J. Y.和Y. Moses，A Guide to Completeness and Complexity for Modular Logics ofKnowledge and Belief，Arti Ficial Intelligence54（1992）.319-379[10] Heuerding，A.，G. Jüager，S. S ch wendimann和M. Seyfried，TheLogicsWork benchLWB：Asnapshot，Euromath Bulletin 2（1996），pp. 177-186。[11] 霍罗克斯岛，FaCT系统，在：H.de Swart，editor，TABLEAUX 1998（1998），pp.307-313[12] 胡斯塔特大学和R.施密特，MSPASS：模态推理的翻译和一阶分辨率，在：R. Dyckho Zedong，editor，TABLEAUX 2000（2000），pp.67比71[13] 耶勒齐姆斯基河，Lua.org[14] van Valkenhoef，G.， 关于OOPS的阐述http://www.ai.rug.nl/~valkenhoef/oops/elaborations.pdf。