Reference : Theorem Provers for Every Normal Modal Logic
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/33698
Theorem Provers for Every Normal Modal Logic
English
Gleißner, Tobias [Freie Universität Berlin > Mathematics and Computer Science]
Steen, Alexander mailto [Freie Universität Berlin > Mathematics and Computer Science]
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
4-May-2017
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Eiter, Thomas
Sands, David
EasyChair
EPiC Series in Computing, Volume 46
14-30
Yes
International
Manchester
UK
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
7 May 2017 to 12 May 2017
Thomas Eiter and David Sands (editors)
[en] Automated Reasoning ; Modal Logic ; Higher Order Modal Logic ; Higher Order Logic
[en] We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined.
By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate.
Researchers ; Professionals ; Students
http://hdl.handle.net/10993/33698
http://easychair.org/publications/paper/340346
46

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Theorem_Provers_For_Every_Normal_Modal_Logic-4.pdfPublisher postprint717.35 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.