English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

On the Saturation of YAGO

MPS-Authors
/persons/resource/persons45573

Suda,  Martin
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45753

Wischnewski,  Patrick
Automation of Logic, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Suda, M., Weidenbach, C., & Wischnewski, P. (2010). On the Saturation of YAGO. In J. Giesl, & R. Hähnle (Eds.), Automated Reasoning (pp. 441-456). Berlin: Springer. doi:10.1007/978-3-642-14203-1_38.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-14BB-9
Abstract
YAGO is an automatically generated ontology out of Wikipedia and WordNet. It is eventually represented in a proprietary flat text file format and a core comprises 10 million facts and formulas. We present a translation of YAGO into the Bernays-Sch¨onfinkel Horn class with equality. A new variant of the superposition calculus is sound, complete and terminating for this class. Together with extended term indexing data structures the new calculus is implemented in Spass-YAGO. YAGO can be finitely saturated by Spass-YAGO in about 1 hour.We have found 49 inconsistencies in the original generated ontology which we have fixed. Spass-YAGO can then prove non-trivial conjectures with respect to the resulting saturated and consistent clause set of about 1.4 GB in less than one second.