llllvvuu/AIPS_inequalities

该数据集包含由AIPS推理引擎生成的合成定理。每个定理都是一个关于实数的三变量非严格不等式（不包含多个不等式的系统）。数据集最初以Python的.pkl格式上传，现在以.txt和.parquet格式提供。每个文件每行包含一个美观打印的表达式，还有一些文件包含`srepr`打印输出。

This dataset contains synthetic theorems generated by AIPS deduction engine. Each theorem is a single inequality (there are no systems of multiple inequalities). Each inequality is a non-strict three-variable inequality over the reals. The original upload was in Python .pkl format. This upload is in .txt and .parquet format. Each file has one pretty-printed expression per row. There are also files with `srepr` printouts.

原始信息汇总

数据集概述

基本信息

• 许可证: cc-by-nc-sa-2.0
• 语言: 英语
• 标签:
  • 合成数据
  • 数学
• 数据规模: 100K<n<1M

数据配置

• 配置名称: srepr
  • 数据文件: inequalities-srepr.parquet
• 配置名称: prettyprint
  • 数据文件: inequalities.parquet

数据描述

• 数据来源: 由AIPS推导引擎生成的合成定理。
• 定理类型: 每个定理是一个单一的不等式（没有多个不等式的系统）。
• 不等式类型: 非严格的三变量不等式，定义在实数域上。
• 原始格式: 最初以Python .pkl格式上传。
• 当前格式: 以.txt和.parquet格式上传。
• 文件内容: 每个文件每行包含一个格式化的表达式。

示例代码

• 示例代码: 用于将数据加载到sympy 1.13.0（Python 3.12.3）或Lean 4中。