This paper describes a simple yet generic database implementation framework for medium sized datasets, as they occur during tests and applications of automated theorem provers. The implementation covers automatic extraction of database objects from a set of text files, a text-based interface for simple database operations, and a tool for document, report and Webpage generation. This paper refers to a database of SETHEO proof data (Setheodb) as an example. It concludes with the description of DBFW as a part of the interactive proof system ILF. The paper also serves as offline documentation for the framework.     «

This paper describes a simple yet generic database implementation framework for medium sized datasets, as they occur during tests and applications of automated theorem provers. The implementation covers automatic extraction of database objects from a set of text files, a text-based interface for simple database operations, and a tool for document, report and Webpage generation. This paper refers to a database of SETHEO proof data (Setheodb) as an example. It concludes with the description of DBF...     »