zenodoopen

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 <alexander.steen@uni-greifswald.de> 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

ShareScore

40/100

Overall dataset sharing score

Score breakdown

These five areas show where the dataset supports — or may limit — practical reuse.

Stewardship: 8
Harmonization: 4
Access: 16
Reuse readiness: 8
Engagement: 4

Topics

TPTP Logic Modal logic Evaluation QMLTP Automated Reasoning Data