pmData

一个基于分离的证明系统（即希尔伯特系统）的精选列表，包含分析、证明数据和日志。这些数据是通过pmGenerator生成和处理的，旨在为研究人员提供基础，避免重复工作。A curated list of separated proof systems (i.e., Hilbert-style systems) that encompasses analyses, proof data and logs. All datasets were generated and processed using pmGenerator, designed to provide a foundational resource for researchers and avoid redundant research work.

原始信息汇总

数据集概述：pmData

pmData 是一个基于分离规则（即希尔伯特系统）的证明系统的精选集合，包含分析、证明数据和日志。该数据集通过 pmGenerator 生成详尽且精炼的证明集合，并将大型高压缩证明文件托管于云服务器，通过下载链接提供访问。较小的文件则托管于 GitHub 或 pmGenerator 页面，用于演示目的。此数据共享方式旨在助力研究人员在前人工作的基础上进一步探索，避免重复劳动。

1. 经典蕴涵逻辑

• 系统：Łukasiewicz 的蕴涵公理
  • 片段：C
  • 符号数量：13（最小 1‑基）
  • 公理：((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ))

2. 经典逻辑

• 系统：带有爆炸原理的 Łukasiewicz 蕴涵公理
  • 片段：C‑O
  • 符号数量：13+3 = 16（最小 2‑基）
  • 公理：((ψ→φ)→χ)→((χ→ψ)→(ξ→ψ))；⊥→ψ
• 系统：Meredith 公理（最小 1‑基，片段 C‑N，21 个符号）
• 系统：Walsh 第 1 至第 6 公理（均为最小 1‑基，片段 C‑N，21 个符号）
• 系统：Łukasiewicz (L₁) 系统（片段 C‑N，已知最小 3‑基，11+6+6 = 23 个符号，数据详见 luk‑pmproofs）
  • 公理：(ψ→φ)→((φ→χ)→(ψ→χ))；(¬ψ→ψ)→ψ；ψ→(¬ψ→φ)
• 系统：Łukasiewicz (L₃) 系统（片段 C‑N，5+13+9 = 27 个符号）
  • 公理：ψ→(φ→ψ)；(ψ→(φ→χ))→((ψ→φ)→(ψ→χ))；(¬ψ→¬φ)→(φ→ψ)

3. 经典模态逻辑

• 系统：S5（Łukasiewicz (L₃) 系统的扩展，片段 C‑N‑L，5+13+9+4+10+10 = 51 个符号）
  • 公理：
    • ψ→(φ→ψ)
    • (ψ→(φ→χ))→((ψ→φ)→(ψ→χ))
    • (¬ψ→¬φ)→(φ→ψ)
    • □ψ→ψ
    • □(ψ→φ)→(□ψ→□φ)
    • ¬□¬ψ→□¬□¬ψ（别名 ◇ψ→□◇ψ）

搜集汇总

数据集介绍

构建方式

pmData数据集精心收录了基于分离规则的证明系统（即希尔伯特系统），涵盖经典蕴涵逻辑、经典逻辑与经典模态逻辑等分支。数据集的构建依托于pmGenerator工具，通过穷举与精炼的方式生成证明集合，并将大型高压缩证明文件托管于云服务器，通过下载链接供研究者获取。小型演示文件则直接存储于本仓库或pmGenerator页面。每个证明系统均详细标注了所属逻辑片段、符号数量及公理内容，例如Łukasiewicz的蕴涵公理、Meredith公理以及Walsh的六个公理，从而为后续研究提供坚实且可复用的数据基础。

特点

该数据集的核心特点在于其编排的全面性与系统性。数据集以表格形式清晰展陈各个证明系统的公理数量（如最小单公理基或已知最小三公理基）与符号规模，跨度从13个符号的最小蕴涵系统到51个符号的模态逻辑S5系统。通过提供详尽的分析、证明数据及日志，pmData避免了重复劳动，使研究者能够在前人工作基础上深入探索。此外，数据的压缩与云端托管策略兼顾了访问效率与存储成本，突出了实用性与可扩展性。

使用方法

研究人员可通过pmGenerator工具直接处理pmData中的证明集合，实现证明的生成与分析。使用方式包括通过GitHub页面的链接访问云端存储的大型压缩文件，或直接查看本仓库内的小型演示文件。每个系统页面均提供丰富的交互式环境（如拓扑基数、ND样本信息），便于定制化分析。研究者可依据需求选择不同逻辑片段（如C-N、C-O）或特定公理系统（如Walsh系列），从而高效地探索、复现或扩展相关证明理论，推动分离规则逻辑研究的自动化与深化。

背景与挑战

背景概述

pmData数据集由研究者xamidi于近年创建，旨在系统化整理基于分离规则（detachment）的证明系统（即希尔伯特系统），并提供详尽的证明分析与日志数据。该数据集聚焦于经典蕴涵逻辑、经典逻辑及经典模态逻辑等核心领域，收录了包括Łukasiewicz公理、Meredith公理及Walsh六条公理在内的最小基公理体系。相较于传统手工构造的证明库，pmData通过自动生成与高压缩存储技术，为自动定理证明领域提供了可复现、可扩展的研究基础。其研究问题直指逻辑证明系统的完整性、最小性及互推关系，显著推动了演绎系统自动化验证与比较分析的前沿探索。

当前挑战

pmData面临的核心挑战包括：其一，领域问题中，经典逻辑与模态逻辑的证明系统虽历史悠久，但公理间的等价性证明与最小基发现仍高度依赖手工推导，现有算法在搜索复杂公理组合时易陷入深度组合爆炸，限制了大规模系统的自动分析；其二，构建过程中，生成海量证明数据需平衡完备性与存储效率，例如对21符号公理系统（如Walsh公理）的穷举枚举会产生指数级证明路径，而高压缩存储策略可能导致数据检索与重构的额外计算开销。此外，不同模态逻辑系统（如S5）的公理扩展缺乏统一表示框架，增加了数据跨系统整合与验证的难度。

常用场景

经典使用场景

pmData数据集的核心应用场景在于为命题逻辑、经典逻辑以及模态逻辑中的希尔伯特风格演绎系统提供系统性、可复现的证明数据。研究者可借助该数据集，对基于分离规则的公理系统进行大规模、详尽的定理证明收集与分析，例如探索不同公理化体系的最小公理基、比较证明长度及复杂度的最优性。该数据集特别适用于逻辑学中的元数学研究，为验证和比较浅层与深层定理间的推导关系提供了坚实的实证基础。

实际应用

在实际应用中，pmData为自动定理证明器与形式化验证系统的开发与评测提供了权威的基准测试集。研究人员可据此评估不同推理算法的效率与正确性，尤其是在处理包含否定、蕴含及模态算子等复杂逻辑片段时的性能。此外，该数据集还可用于教育领域，为逻辑学课程提供大量可参考的证明示例，辅助学生理解形式系统的推导过程与结构特性，并促进交互式逻辑推理工具的研发。

衍生相关工作

pmData的发布催生了一系列衍生研究工作，其中最具代表性的是配套工具pmGenerator，它实现了对分离规则系统的高效证明生成与压缩，使得大规模公理化证明数据的产出成为可能。其他相关工作包括针对Łukasiewicz系统L₁和L₃的细化证明分析、luk-pmproofs项目中对经典逻辑公理基的独立验证，以及基于S5模态逻辑的证明模式挖掘。这些工作共同构建了从数据生成到元逻辑研究的完整链条，为后续公理化复杂性分析及分布式证明库的建设奠定了技术基础。