Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics"

These files are associated with the manuscript entitled"Solving Quantified Modal Logic Problems by Translation to Classical Logics"by Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller.

Contact: Alexander Steen <[e-mail]>

Contents-----------

  - QMLTP-monomodal-NX0.tar.gz    This archive contains the TPTP NX0 representations of the 580 mono-modal    problems translated from the QMLTP library [1,2].      - QMLTP-monomodal-TF0-embedded-rigid-local.tar.gz    This archive contains the embedded TF0 files created     from the monomodal NX0 files using the Logic Embedding Tool [3].      - QMLTP-monomodal-TH0-embedded-rigid-local.tar.gz    This archive contains the embedded TH0 files created     from the monomodal NX0 files using the Logic Embedding Tool [3,4].    - QMLTP-multimodal-NX0-and-embedded.tar.gz    This archive contains the TPTP NX0 representations of the 20 multi-modal    problems translated from the QMLTP library [1,2]. Additionally, it    contains the 20 embedded TF0 and the 20 embedded THF files created     from the NX0 files using the Logic Embedding Tool [3,4].      - QMLTP-primary-evaluation-results-QMLTP.zip    This archive contains the primary evaluation data creating from    running E 3.0.03, Leo-III 1.7.8, Nitpick 2016, Vampire 4.8,     MleanCoP 1.3, nanoCoP-M 2.0 on the problem files.    All reasoning systems except Nitpick were run on the StarExec Miami cluster with a 60s    wall clock and 480 CPU time limit. The StarExec Miami computers have an    octa-core Intel Xeon E5-2667 3.20 GHz CPU, 128 GiB memory, and run the    CentOS Linux release 7.4.1708 operating system. Nitpick was run on a server    with a 60s wall clock time limit. The server has an octa-core Intel Xeon E5-    2609 2.50 GHz CPU, 64 GiB memory, and the CentOS Linux release 7.9.2009    operating system.    - README    This file.            [1] T. Raths and J. Otten. The QMLTP Problem Library for First-Order Modal Logics.    In B. Gramlich, D. Miller, and U. Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning,    number 7364 in Lecture Notes in Artificial Intelligence, pages 454–461. Springer, 2012.[2] http://www.iltp.de/qmltp/[3] A. Steen. An extensible logic embedding tool for lightweight non-classical reasoning (short paper).    In B. Konev, C. Schon, and A. Steen, editors, Proceedings of the 8th Workshop on Practical Aspects of Automated    Reasoning, number 3201 in CEUR Workshop Proceedings, 2022.[4] https://github.com/leoprover/logic-embedding