GLUE: Opening the world to theorem provers

GLUE is a system to combine heterogeneous and distributed sources of information with a deductive kernel. For this purpose access methods for external sources of information, like databases, can be specified. Pieces of a program are generated from such a specification which can be used also in other programs. This technique has been developed with an application to theorem provers in mind. We will show how GLUE can be used either stand-alone or together with a theorem prover like PROTEIN to solve real world problems. Some examples of problems utilizing such a combination are presented.