| Solving Software Reuse Problems with Theorem Provers (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. For a challenging application, the software component retrieval, we present a powerful solution by combining two systems. The NORA/HAMMR-tool handles all aspects concerning with the logical representation of the application problem, the ILF-tool provides an infrastructure to apply several ATPs like SETHEO, OTTER, SPASS to the emerging deductive problems. For a fruitful practically application, however, an adjustment of application dependent parameter is advisable. The parameter settings can be obtained from a little test suite, if some general tools, already integrated in ILF, for analysation of emerged proof tasks are exploited. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||