数据集概述
该数据集包含布尔部分多态性验证的相关文件，围绕特定三元布尔合取函数f是否保持两种布尔关系（ΓL₀(χ₂)、ΓL₂(χ₃)）的问题展开，通过将问题转化为SMT-LIB2.0格式并使用Z3求解器验证，提供了问题实现文件、求解器输出及形式化证明等内容。
文件详解
- f-pPol-GammaL0chi2-GammaL2chi3.z3：SMT-LIB2.0格式的问题实现文件，用于Z3等求解器运行
- z3-output.txt：Z3求解器运行上述.z3文件后的输出结果
- f-preserves-GammaL0chi2_proof.txt：Z3生成的f保持ΓL₀(χ₂)的形式化证明文件
- f-preserves-GammaL2chi3_proof.txt：Z3生成的f保持ΓL₂(χ₃)的形式化证明文件
- partial_polymorphisms.pdf：问题及数据集的详细描述文档
- partial_polymorphisms.tex：生成partial_polymorphisms.pdf的LaTeX源文件
适用场景
- 布尔函数与多态性研究：验证特定布尔函数对布尔关系的保持性
- 自动定理证明应用：分析Z3求解器在形式化证明中的应用效果
- 逻辑与代数计算研究：探究布尔代数中部分多态性的验证方法
- 计算机科学教育：作为布尔逻辑、自动推理相关课程的案例数据
