Automated Reasoning with Very Large Theories

VLT是一种用逻辑语言表示的形式化知识的集合。例如，这样的VLT可以通过程序从某个领域的大量文档集合(如生物学)或从大量网站集合中提取。使用这样的理论推理意味着基于知识的逻辑语义而不是关键字搜索来回答查询。如果该项目被证明是成功的，它可能会产生一种新的Web搜索方式，其中对用户的查询的搜索将基于语义和推理。

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.