| 2 (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. We describe a combination of the NORA/HAMMR software component retrieval tool and the ILF system which provides the necessary infrastructure to apply different first-order theorem provers to the emerging proof problems. This framework allows the cooperation of independent deductive subsystems in two different modes. Our results show that both modes---competition between problem variants or provers and proper cooperation following the TECHS approach---improve the success rate considerably. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||