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.
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,James, Holden,Sean, and Paulson,Lawrence. (2013). First-order theorem proving. UCI Machine Learning Repository. https://doi.org/10.24432/C5RC9X.
@misc{misc_first-order_theorem_proving_249,
author = {Bridge,James, Holden,Sean, and Paulson,Lawrence},
title = {{First-order theorem proving}},
year = {2013},
howpublished = {UCI Machine Learning Repository},
note = {{DOI}: 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.