MiG

Implementing and Evaluating Provers for First-order Modal Logics

C. 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
VerfasserC. Benzmüller, Jens Otten, Thomas Raths
VerlagIOS Press Ebooks
ThemaHigher Order Logic, Semantic Embedding, Modal Logics, Automated Reasoning
Datum2012
Kennunghttp://dx.doi.org/10.3233/978-1-61499-098-7-163
Quelle/n
Erschienen inFrontiers in Artificial Intelligence and Applications, Volume 242: ECAI 2012
Spracheeng
ArtText
Größe oder Längepp. 163-168