The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
Negin Arhami, Geoff Sutcliffe · EPiC series in computing · 2018
Many Automated Theorem Prover (ATP) systems for different logics, and translators for translating different logics from one to another, have been developed and are now available. Some logics are more expressive than others, and it is easier to express problems in those logics. On the other hand, the ATP systems for less expressive logics have been under development for many years, and are more powerful and reliable. There is a trade-off between expressivity of a logic, and the power and reliability of the available ATP systems. Translators and ATP systems can be combined to try to solve a problem. In this research, an experiment has been carried out to compare the performance of difference combinations of translators and ATP systems.