| Abstract: | 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. |
