Solving QMLTP Problems
by Translation to Higher-order Logic
Abstract
This work describes an evaluation of Automated Theorem Proving (ATP) systems
on problems taken from the QMLTP library of first-order modal logic problems.
Principally, the problems are translated to higher-order logic in the TPTP
languages using an embedding approach, and solved using higher-order logic
ATP systems.
Additionally, the results from native modal logic ATP systems are considered,
and compared with those from the embedding approach.