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.

In the short term the users and beneficiaries of the research are in the academic research community. The research area is too young to have immediate short-term impact outside the community. Let us point out potential longer-term impact. The very nature of our project is answering in real time queries to very large collections of knowledge. This is not very different from what Web search engines do. What is different is the way HOW queries are answered: in our case answering is based on semantics and reasoning. The apparent connection between search engine query answering and reasoning with Very Large THeories (VLTs) suggests that the potential impact of our project goes far beyond automated reasoning and that in the long term potential beneficiaries of our project include nearly everybody using computers. To realise this longer-term impact we intend to maintain collaboration with the developers of VLTs. The collaboration will be of the following kind: (1) We will use their VLTs for developing and benchmarking our system. (2) We will try to integrate the system in their Web interfaces and use it as (one of) mechanisms for query answering. This will enable us to understand what kinds of queries are posed by the users and benchmark our system against the queries. We are also going to analyse queries posed by users and answers to them. These queries and answers will be key to understanding how semantic Web search can be used when the standard Web search is inadequate. Another potential avenue to exploit is contacts with the natural language processing researchers. The idea is to try to extract formal knowledge from parsed natural language texts and use theorem provers to answer queries, check consistency, or extract new knowledge. This is a separate line of research that can complement this project and we plan a separate grant proposal for it. It is also important for us to present our results at world-leading conferences attracting industrial participants, such as WWW and IJCAI. We will submit publications resulting from this project to these conferences and collocated workshops. Visits to research centres developing VLTs and the conferences mentioned above are included in this proposal. Apart from the visits, there are no other resource implications resulting from implementing the impact activities.