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:  

Multivariate

Number of Instances:

6118

Area:

Computer

Attribute Characteristics:

Real

Number of Attributes:

51

Date Donated

2013-04-17

Associated Tasks:

Classification

Missing Values?

N/A

Number of Web Hits:

50862

Source:

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
UK

+44 (0)1223 763500
forename.surname '@' cl.cam.ac.uk


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