Notes of the ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution-猫眼课题宝

ECAI-10 关于上下文和本体进化的自动推理研讨会的笔记

DOI：

发表时间：

2010

期刊：

影响因子：

通讯作者：

中科院分区：

文献类型：

作者：

A. Bundy;Jos Lehmann;G. Qi;I. Varzinczak

使用嵌入式公式进行推理与SUMO本体相关，但迄今为止对自动化的支持有限。我们研究了高阶自动定理证明是否适用于该任务。此外，我们指出了我们在实验中揭示的一个挑战：相扑中的模态运算符与布尔扩展性相冲突。提出了解决方案。开源的建议上合并本体（SUMO）[9]（以及类似的专有Cyc[13]）包含少量但重要的高阶表示。在这些系统中，解决高阶挑战的方法是采用特定的翻译“技巧”，可能与一些预处理技术相结合或另外使用。这种方法的例子是SUMO b[11]中使用的嵌入式公式引用技术和CYC[13]中的启发式级模块。然而，不幸的是，这些解决方案非常有限。其结果是，目前不支持许多理想的推断，因此许多相关查询无法回答。这包括将公式嵌入作为术语参数的语句，例如，使用诸如believe或knows这样的认知运算符的语句，使用诸如holdduring这样的时态运算符的语句，以及诸如disapprove或hasPurpose这样的进一步运算符的语句。虽然SUMO的一阶自动定理证明（FOATP）最近有了很大的改进，但对于非平凡嵌入公式的推理仍然只有非常有限的支持；我们给出一个例子（前提中的自由变量是全称的，而查询中的自由变量是存在的）：例1（时间上下文中的推理）。任何时候都是如此。玛丽喜欢比尔。2009年，玛丽喜欢谁，苏就喜欢谁。有哪一年苏喜欢过某个人吗？A: => ？在…期间？Y ?B:（像玛丽·比尔一样）C:（在2009年期间）（对所有人）？（=>）像玛丽一样？(比如苏？X))))问：（持有期间）？Y)(比如苏？X))这个例子，这是FO-ATP的一个挑战（注意嵌入的一阶公式），实际上对于高阶自动定理证明者（HO-ATP）来说是微不足道的：证明者LEO-II[5]可以在0.16解决它。这项工作由德国研究基金会资助，资助BE 2501/6-1。2 . articelsoftware，电子邮件：cbenzmueller|apease@articulatesoftware.com 3 . SUMO可在http://www.ontologyportal.org获得4 .为了节省空间，“喜欢”被写成“喜欢”。在标准的MacBook上。由LEO-II在0.08秒内证明的Ex.1的一个轻微修改是：Ex. 2 （Ex.1修改；A被“True always成立”取代）。A：在…期间？B:（像玛丽·比尔一样）C:（在2009年期间）（对所有人）？（=>）像玛丽一样？(比如苏？X))))问：（持有期间）？Y)(比如苏？X))在[6]中研究了进一步的例子；在这里，我们还概述了从上面使用的相扑的SUO-KIF表示语言[10,7]到包括LEO-II在内的几个ho - atp支持的新的高阶TPTP THF语法[14]的翻译。例1和例2的有效性很容易证明，只要假设布尔可拓性（这确保每个公式的外延，包括嵌入的公式，要么为真，要么为假）。这个假设在SUMO中从未被质疑过，无论是[7]还是[10]。然而，这个假设也会导致有问题的结果，正如下面对例2的轻微修改所说明的那样：例3（例2被修改；现在为经验背景而制定）A ":(知道？（真的）B:（像玛丽·比尔一样）C:（认识克里斯）？（=>）像玛丽一样？(比如苏？使用布尔可拓性，查询很容易显示有效，LEO-II可以在0.04秒内证明它。然而，现在这个推论令人不安，因为我们没有明确要求（知道Chris（像Mary Bill））持有，这在直觉上似乎是强制性的。因此，我们在这里（重新）发现了一些逻辑学家可能声称众所周知的问题：在经典的扩展高阶逻辑中，必须非常小心地处理模态。因此，我们正在进行的工作是研究如何适当地调整相扑运动中受影响模式的建模，以适当地解决这一问题。下面是一个相应的建议。值得注意的是，A '中的True实际上可以被其他重言式代替，例如（equal Mary Mary）；这可能看起来更自然，这个例子仍然可以用LEO-II以毫秒为单位来证明。关于经典高阶逻辑中泛函和布尔可拓性的详细讨论，我们参考[2]。ARCOE-10研讨会笔记

Reasoning with embedded formulas is relevant for the SUMO ontology but there is limited automation support so far. We investigate whether higher-order automated theorem provers are applicable for the task. Moreover, we point to a challenge that we have revealed as part of our experiments: modal operators in SUMO are in conflict with Boolean extensionality. A solution is proposed. 1 EMBEDDED FORMULAS IN SUMO The open source Suggested Upper Merged Ontology (SUMO) [9] (and similarly, proprietary Cyc [13]) contains a small but significant amount of higher-order representations. The approach taken in these systems to address higher-order challenges has been to employ specific translation ’tricks’, possibly in combination or in addition to some pre-processing techniques. Examples of such means are the quoting techniques for embedded formulas as employed in SUMO [11] and the heuristic-level modules in CYC [13]. Unfortunately, however, these solutions are strongly limited. The effect is that many desirable inferences are currently not supported, so that many relevant queries cannot be answered. This includes statements in which formulas are embedded as arguments of terms, for example, statements that employ epistemic operators such as believes or knows, temporal operators such as holdsDuring, and further operators such as disapproves or hasPurpose. While first-order automated theorem proving (FOATP) for SUMO has strongly improved recently [12], there is still only very limited support for reasoning with non-trivial embedded formulas; we give an example (free variables in premises are universal and those in the query are existential): Ex. 1 (Reasoning in temporal contexts.) What holds that holds at all times. Mary likes Bill. During 2009 Sue liked whoever Mary liked. Is there a year in which Sue has liked somebody? A: (=> ?P (holdsDuring ?Y ?P)) B: (lk Mary Bill) C: (holdsDuring (YearFn 2009) (forall (?X) (=> (lk Mary ?X) (lk Sue ?X)))) Q: (holdsDuring (YearFn ?Y) (lk Sue ?X)) This example, which is a challenge for FO-ATP (note the embedded first-order formula), is actually trivial for higher-order automated theorem provers (HO-ATP): the prover LEO-II [5] can solve it in 0.16 1 This work is funded by the German Research Foundation under grant BE 2501/6-1. 2 Articulate Software, email: cbenzmueller|apease@articulatesoftware.com 3 SUMO is available at http://www.ontologyportal.org 4 To save space ’likes’ is written as ’lk’. sec. on a standard MacBook. A slight modification of Ex.1, which LEO-II proves in 0.08 sec., is: Ex. 2 (Ex.1 modified; A is replaced by ’True always holds’.) A’: (holdsDuring ?Y True) B: (lk Mary Bill) C: (holdsDuring (YearFn 2009) (forall (?X) (=> (lk Mary ?X) (lk Sue ?X)))) Q: (holdsDuring (YearFn ?Y) (lk Sue ?X)) Further examples are studied in [6]; there we also outline the translation from SUMO’s SUO-KIF representation language [10, 7] as used above to the new higher-order TPTP THF syntax [14] as supported by several HO-ATPs including LEO-II. 2 THE PROBLEM WITH MODAL OPERATORS Validity of Ex.1 and Ex.2 is easily shown provided that Boolean extensionality is assumed (this ensures that the denotation of each formula, also the embedded ones, is either true of false). This assumption has actually never been questioned for SUMO, neither in [7] nor in [10]. However, this assumption also leads to problematic effects as the following slight modification of Ex.2 illustrates: Ex. 3 (Ex.2 modified; now formulated for an epistimec context) A”: (knows ?Y True) B: (lk Mary Bill) C’: (knows Chris (forall (?X) (=> (lk Mary ?X) (lk Sue ?X))) Q’: (knows Chris (lk Sue Bill)) Using Boolean extensionality the query is easily shown valid and LEO-II can prove it in 0.04 sec. However, now this inference is disturbing since we have not explicitly required that (knows Chris (lk Mary Bill)) holds which intuitively seems mandatory. Hence, we here (re-)discover an issue that some logicians possibly claim as widely known: modalities have to be treated with great care in classical, extensional higher-order logic. Our ongoing work therefore studies how we can suitably adapt the modeling of affected modalities in SUMO in order to appropriately address this issue. A respective proposal is sketched next. 5 It is important to note that True in A’ can actually be replaced by other tautologies, e.g. by (equal Mary Mary); this may appear more natural and the example can still be proved by LEO-II in milliseconds. 6 For a detailed discussion of functional and Boolean extensionality in classical higher-order logic we refer to [2]. ARCOE-10 Workshop Notes

Notes of the ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution

ECAI-10 关于上下文和本体进化的自动推理研讨会的笔记

文献摘要

被引文献

相似文献