Search
 
loader loading subjects...
cover
Implementing and Evaluating Provers for First-order Modal Logics
Christoph Benzmüller, Jens Otten, Thomas Raths
163 - 168
10.3233/978-1-61499-098-7-163
Frontiers in Artificial Intelligence and Applications
Volume 242: ECAI 2012
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 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.

Download
Creative Commons License