Automated Reasoning with Very Large Theories

点击翻译按钮获取中文摘要

Our proposal focuses on first-order reasoning with Very Large Theories (VLTs).A VLT is a collection of formalised knowledge expressed in a logical language.For example, such a VLT can be extracted by programs from largecollections of documents in some domain, such as biology, or from a largecollection of Web sites.Reasoning with such theories means answering queries based on thelogical semantics of the knowledge as opposed to the keyword search.If the project turns out to be successful, it may give rise to new waysof Web search where search for user's queries will be based onsemantics and reasoning.