数据集概述
本数据集围绕整数分拆格（按支配序排列）及其在形式概念分析中的标准上下文展开，提供了n=9分拆格的标准上下文无法嵌入n=10分拆格的相关证据，包含证明文件、计算输出及说明文档等资料。
文件详解
- 说明文档与源码：
- context_embeddings.pdf：PDF格式，提供数据集背景及文件详细说明
- context_embeddings.tex：TeX格式，context_embeddings.pdf的源码文件
- 计算输出文件：
- embedK9K10_int.out：.out格式，整数模式下n=9嵌入n=10的计算输出
- embedK9K10.out：.out格式，n=9嵌入n=10的计算输出
- 形式验证文件：
- embedK9K10_int.z3：.z3格式，整数模式下的形式验证文件
- embedK9K10.z3：.z3格式，标准模式下的形式验证文件
- 不可嵌入性证明文件：
- noK9K10_int.proof：.proof格式，整数模式下n=9无法嵌入n=10的证明文件
- noK9K10.proof：.proof格式，标准模式下n=9无法嵌入n=10的证明文件
适用场景
- 形式概念分析研究：验证分拆格标准上下文的嵌入关系
- 离散数学研究：分析整数分拆格的结构性质
- 计算逻辑研究：探究形式验证工具在格嵌入问题中的应用
- 数学证明自动化研究：基于不可嵌入性证明文件开发相关算法
