Springe direkt zu Inhalt

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.

Titel
Provers for First-order Modal Logics
Verfasser
Christoph Benzmüller, Jens Otten, Thomas Raths
Verlag
IOS Press Ebooks
Schlagwörter
Higher Order Logic, Semantic Embedding, Modal Logics, Automated Reasoning
Datum
2012
Kennung
http://dx.doi.org/10.3233/978-1-61499-098-7-163
Erschienen in
Frontiers in Artificial Intelligence and Applications, Volume 242: ECAI 2012
Sprache
eng
Art
Text
Größe oder Länge
pp. 163-168