A Contextual Approach to Detection of Conflicting Ontologies
Jos Lehmann · 2010
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 ap- plicable 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 spe- cific 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 rele- vant queries cannot be answered. This includes statements in which formulas are embedded as argu- ments of terms, for example, statements that employ epistemic op- erators such as believes or knows, temporal operators such as holdsDuring, and further operators such as disapproves or hasPurpose. While first-order automated theorem proving (FO- ATP) 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 univer- sal 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 the- orem 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|[email protected] 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 transla- tion 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 PROBLEMWITH MODAL OPERATORS Validity of Ex.1 and Ex.2 is easily shown provided that Boolean ex- tensionality is assumed (this ensures that the denotation of each for- mula, also the embedded ones, is either true of false). This assump- tion 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 dis- turbing 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, ex- tensional 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 (equalMaryMary); 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 clas- sical higher-order logic we refer to [2]. ARCOE-10 Workshop Notes