STIRDAT: A system tightly integrating relational databases and a theorem prover

There has been a growing awareness of the need to share data and services a mong autonomous heterogeneous information sources. For obvious reasons, the se sources are storing information in ways that meet their own needs and he nce in different formats. However, for a combination of information from he terogeneous sources to be truly useful, a user needs to be able to use the shared information without having to learn the particular data format or th e locations of the relevant data. This idea can be taken a step further as the importance of combining techni ques from various areas in computer science becomes more obvious. There are a number of benefits that can be derived from combining, for example, some of the features of Artificial Intelligence systems, such as logical infere nce, with those of traditional database systems. This paper describes STIRD AT, a system tightly and transparently integrating data in a number of rela tional databases stored at different sites with a theorem prover. It provid es a clear illustration of the benefits to be gained from a system combinin g techniques that have proven independently useful in different areas of Co mputer Science. (C) 2000 Elsevier Science B.V. All rights reserved.