Implementing and evaluating provers for first-order modal logics

Abstract. While there is a broad literature on the theory of first-order modal logics, little is known about practical reasoning systems for them. This paper presents several implementations of fully auto-mated theorem provers for first-order modal logics based on different proof calculi. Among these calculi are the standard sequent calculus, a prefixed tableau calculus, an embedding into simple type theory, an instance-based method, and a prefixed connection calculus. All im-plementations are tested and evaluated on the new QMLTP problem library for first-order modal logic.