数据集概述
该数据集包含论文《SATPin: Axiom Pinpointing for Lightweight Description Logics through Incremental SAT》中提出的程序的实证评估结果及对应输入数据，支持轻量级描述逻辑领域的公理定位方法研究。
文件详解
该数据集包含八个文件，具体说明如下：
- 文本数据文件（.txt格式，共4个）：
- YNall.txt：包含实验数据记录，字段示例有inst（实例）、num_min（最小数量）、restarts（重启次数）、time（时间）、memory（内存）、ontology（本体）、type（类型）等
- all-times.txt：可能记录所有实验的时间数据
- Mall.txt：可能为实验相关的综合数据文件
- all-times-SATPin.txt：可能记录SATPin方法的时间数据
- 文档文件（.pdf格式，共3个）：
- onecactus.pdf：可能为实验相关的文档或图表
- cactusriss.pdf：可能为实验相关的文档或图表
- MinAs.pdf：可能为实验相关的文档或图表
- 代码文件（.r格式，共1个）：
- cleanAnalysis.R：R语言代码文件，可能用于数据清理与分析
适用场景
- 描述逻辑研究：用于分析轻量级描述逻辑中公理定位方法的性能
- 增量SAT算法评估：支持对增量SAT技术在公理定位任务中的效率验证
- 实证研究复现：为复现相关论文的实验结果提供数据支持
- 逻辑推理性能分析：可用于研究推理算法的时间、内存等资源消耗特征
