QMLTP library

该数据集是由QMLTP库提供的，包含了来自一阶模态逻辑的问题，涵盖了混合应用、哥德尔编码、多模态逻辑、将经典逻辑视为模态逻辑以及语法模态逻辑问题等多个领域。数据集被划分为五个组别：APM（10个问题）、G??领域（245个问题）、MML（20个问题）、NLP（5个问题）、SET（75个问题）以及SYM（245个问题）。每个问题都附有针对一阶模态逻辑属性各种组合的预期结果。总共有600个问题。这项任务的目的是评估自动定理证明系统在模态逻辑问题上的表现。

This dataset is provided by the QMLTP library, which comprises problems from first-order modal logic spanning multiple domains including hybrid applications, Gödel encoding, multimodal logic, treating classical logic as modal logic, and syntactic modal logic problems. The dataset is divided into five groups: APM (10 problems), G?? domain (245 problems), MML (20 problems), NLP (5 problems), SET (75 problems), and SYM (245 problems). Each problem is accompanied by expected results for various combinations of first-order modal logic properties. In total, the dataset contains 600 problems. The objective of this task is to evaluate the performance of automated theorem proving systems on modal logic problems.