| Date: | 2017, March 15 |
| Author: | Kuksa, Eugen |
| Title: | Logic-independent Premise Selection for Automated Theorem Proving in Ontohub |
Formalisations of problems using first-order logic often result in large collections of theories. The repository engine Ontohub provides structuring, version control, web-based editing and maintenance as well as proof support for theories through interfacing with standard TPTP provers. In order to speed up the proving process, premises can be selected automatically, which significantly can reduce the proving time. State of the art premise selections operate on one logic only or are even tightly coupled with a prover. This work leverages this limitation and shows how to select premises on theories in arbitrary logics and use them with arbitrary provers.