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


Repository Web            Google
View ALL Data Sets

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:

42861

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