Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics"
DOI10.5281/zenodo.10802221Zenodo10802221MaRDI QIDQ6709659FDOQ6709659
Dataset published at Zenodo repository.
Geoff Sutcliffe, Alexander Steen, Christoph Benzmüller
Publication date: 10 March 2024
Copyright license: Creative Commons Attribution 4.0 International
These files are associated with the manuscript entitled"Solving Quantified Modal Logic Problems by Translation to Classical Logics"by Alexander Steen, Geoff Sutcliffe, Christoph Benzmller. 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 454461. 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
This page was built for dataset: Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics"
