Authors ' Addresses

Publi ation Notes This report is an extended version of an arti le intended for publi ation elsewhere. Abstra t YAGO is an automati ally generated ontology out of Wikipedia and Word-Net. It is eventually represented in a proprietary at text le format and a ore omprises 10 million fa ts and formulas. We present a translation of YAGO into the Bernays-S honnkel Horn lass with equality. A new vari-ant of the superposition al ulus is sound, omplete and terminating for this lass. Together with extended term indexing data stru tures the new al-ulus is implemented in Spass-YAGO. YAGO an be nitely saturated by Spass-YAGO in about 1 hour. We have found 49 in onsisten ies in the orig-inal generated ontology whi h we have xed. Spass-YAGO is able to prove non-trivial onje tures with respe t to the resulting saturated and onsistent lause set of about 1.4 GB in less than one se ond. Keywords superposition, large nite domain reasoning, reasoning in large ontologies