CASC 2023 Benchmarks

该数据集包含了500个同态的一阶基准测试用例，这些用例专门用于测试不同定理证明中的微积分实现。这些基准测试用例被分为不含等式的FNE类别和含等式的FEQ类别，所有用例均为定理。数据集的规模为500个基准测试，任务是对这些定理进行证明。This dataset includes 500 homomorphic first-order benchmark test cases, which are specifically designed to evaluate calculus implementations across various theorem proving systems. These benchmark cases are categorized into two groups: FNE (First-order without Equality) and FEQ (First-order with Equality). All these test cases are formalized as theorems. The dataset consists of 500 benchmarks in total, with the assigned task being to prove these respective theorems.