Propositional_Resolution_Based命题归结证明数据集

数据集概述

本数据集包含命题归结证明，主要采用SMT求解器VeriT格式，同时包含少量TraceCheck格式证明和一份DRUP/DRAT格式证明。这些证明曾用于Skeptik工具中证明压缩算法的评估实验，为命题逻辑证明相关研究提供基础数据。

文件详解

• 文件名称：Propositional Resolution Proofs.zip
• 文件格式：ZIP
• 字段映射介绍：压缩包内包含多种格式的命题归结证明文件，主要格式为VeriT，少量为TraceCheck，另有一份DRUP/DRAT格式证明；具体字段需解压后根据各证明格式的规范查看，原数据未提供预览内容。

适用场景

• 命题逻辑证明压缩算法研究: 用于评估和优化Skeptik工具等平台中的证明压缩算法性能。
• 证明格式兼容性分析: 对比VeriT、TraceCheck、DRUP/DRAT等不同命题归结证明格式的结构差异与转换可行性。
• SMT求解器输出验证: 验证VeriT等SMT求解器生成的命题归结证明的正确性与完整性。
• 自动推理工具测试: 为命题逻辑领域的自动推理工具提供标准化的证明数据测试集。