Center for Machine Learning and Intelligent Systems
About  Citation Policy  Donate a Data Set  Contact

Repository Web            Google
View ALL Data Sets

× Check out the beta version of the new UCI Machine Learning Repository we are currently testing! Contact us if you have any issues, questions, or concerns. Click here to try out the new site.

First-order theorem proving Data Set
Download: Data Folder, Data Set Description

Abstract: 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.

Data Set Characteristics:  


Number of Instances:




Attribute Characteristics:


Number of Attributes:


Date Donated


Associated Tasks:


Missing Values?


Number of Web Hits:



James P Bridge, Sean B Holden and Lawrence C Paulson

University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD

+44 (0)1223 763500
forename.surname '@'

Data Set Information:

See the file bridge-holden-paulson-details.txt in the submitted tarball.

Attribute Information:

The attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details.

Relevant Papers:

Machine learning for first-order theorem proving: learning to select a good heuristic
James P Bridge, Sean B Holden and Lawrence C Paulson
Submitted for publication in the Journal of Automated Reasoning, Springer 2012/13.

Citation Request:

Please cite the paper if you use this data set.

Supported By:

 In Collaboration With:

About  ||  Citation Policy  ||  Donation Policy  ||  Contact  ||  CML