First-order theorem proving
Donated on 4/16/2013
Given a theorem, predict which of five heuristics will give the fastest proof when used by a first-order prover. A sixth prediction declines to attempt a proof, should the theorem be too difficult.
Dataset Characteristics
Multivariate
Subject Area
Computer Science
Associated Tasks
Classification
Feature Type
Real
# Instances
6118
# Features
-
Dataset Information
Additional Information
See the file bridge-holden-paulson-details.txt in the submitted tarball.
Has Missing Values?
No
Variables Table
| Variable Name | Role | Type | Description | Units | Missing Values |
|---|---|---|---|---|---|
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no | |||||
| no |
0 to 10 of 51
Additional Variable Information
The attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details.
Dataset Files
| File | Size |
|---|---|
| ml-prove.tar.gz | 1.1 MB |
Reviews
There are no reviews for this dataset yet.
pip install ucimlrepo
from ucimlrepo import fetch_ucirepo # fetch dataset first_order_theorem_proving = fetch_ucirepo(id=249) # data (as pandas dataframes) X = first_order_theorem_proving.data.features y = first_order_theorem_proving.data.targets # metadata print(first_order_theorem_proving.metadata) # variable information print(first_order_theorem_proving.variables)
Bridge, J., Holden, S., & Paulson, L. (2012). First-order theorem proving [Dataset]. UCI Machine Learning Repository. https://doi.org/10.24432/C5RC9X.
Creators
James Bridge
Sean Holden
Lawrence Paulson
DOI
License
This dataset is licensed under a Creative Commons Attribution 4.0 International (CC BY 4.0) license.
This allows for the sharing and adaptation of the datasets for any purpose, provided that the appropriate credit is given.