Implementing and Evaluating Provers for First-order Modal Logics

Christoph Benzmüller, Jens Otten, Thomas Raths— 2012

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 automated 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 implementations are tested and evaluated on the new QMLTP problem library for first-order modal logic.

TitelProvers for First-order Modal Logics
VerfasserChristoph Benzmüller, Jens Otten, Thomas Raths
VerlagIOS Press Ebooks
ThemaHigher Order Logic, Semantic Embedding, Modal Logics, Automated Reasoning
Erschienen inFrontiers in Artificial Intelligence and Applications, Volume 242: ECAI 2012
Größe oder Längepp. 163-168