Paper published in a book (Scientific congresses, symposiums and conference proceedings)
Theorem Provers for Every Normal Modal Logic
Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph
2017In Eiter, Thomas; Sands, David (Eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Peer reviewed
 

Files


Full Text
Theorem_Provers_For_Every_Normal_Modal_Logic-4.pdf
Publisher postprint (734.57 kB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Automated Reasoning; Modal Logic; Higher Order Modal Logic; Higher Order Logic
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Gleißner, Tobias;  Freie Universität Berlin > Mathematics and Computer Science
Steen, Alexander ;  Freie Universität Berlin > Mathematics and Computer Science
Benzmüller, Christoph ;  University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
External co-authors :
yes
Language :
English
Title :
Theorem Provers for Every Normal Modal Logic
Publication date :
04 May 2017
Event name :
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Event organizer :
Thomas Eiter and David Sands (editors)
Event date :
7 May 2017 to 12 May 2017
Audience :
International
Main work title :
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Editor :
Eiter, Thomas
Sands, David
Publisher :
EasyChair, Manchester, United Kingdom
Collection name :
EPiC Series in Computing, Volume 46
Pages :
14-30
Peer reviewed :
Peer reviewed
Commentary :
46
Available on ORBilu :
since 14 December 2017

Statistics


Number of views
104 (2 by Unilu)
Number of downloads
398 (6 by Unilu)

Bibliography


Similar publications



Contact ORBilu