DEVELOPMENT... OpenML
Data
first-order-theorem-proving

first-order-theorem-proving

active ARFF Publicly available Visibility: public Uploaded 22-05-2015 by unknown
0 likes downloaded by 0 people , 0 total downloads 0 issues 0 downvotes
  • OpenML-CC18 OpenML100 study_123 study_14 study_34 study_50 study_52 study_7 study_98 study_99 study_225 study_236 study_293 study_270 study_271 study_253 study_282 study_275
Issue #Downvotes for this reason By


Loading wiki
Help us complete this description Edit
Author: James P Bridge, Sean B Holden and Lawrence C Paulson Source: [UCI](https://archive.ics.uci.edu/ml/datasets/First-order+theorem+proving) Please cite: James P Bridge, Sean B Holden and Lawrence C Paulson . Machine learning for first-order theorem proving: learning to select a good heuristic. Journal of Automated Reasoning, Springer 2012/13. 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 dataset file. Attribute Information: The attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details.

52 features

Class (target)nominal6 unique values
0 missing
V28numeric1023 unique values
0 missing
V27numeric4560 unique values
0 missing
V29numeric4709 unique values
0 missing
V30numeric69 unique values
0 missing
V31numeric79 unique values
0 missing
V32numeric82 unique values
0 missing
V33numeric23 unique values
0 missing
V34numeric31 unique values
0 missing
V35numeric48 unique values
0 missing
V36numeric70 unique values
0 missing
V37numeric1053 unique values
0 missing
V38numeric1569 unique values
0 missing
V39numeric893 unique values
0 missing
V40numeric72 unique values
0 missing
V41numeric1041 unique values
0 missing
V42numeric37 unique values
0 missing
V43numeric29 unique values
0 missing
V44numeric1698 unique values
0 missing
V45numeric2246 unique values
0 missing
V46numeric1941 unique values
0 missing
V47numeric1676 unique values
0 missing
V48numeric1703 unique values
0 missing
V49numeric2315 unique values
0 missing
V50numeric1537 unique values
0 missing
V51numeric2462 unique values
0 missing
V14numeric82 unique values
0 missing
V2numeric1194 unique values
0 missing
V3numeric1148 unique values
0 missing
V4numeric1261 unique values
0 missing
V5numeric1394 unique values
0 missing
V6numeric1030 unique values
0 missing
V7numeric1309 unique values
0 missing
V8numeric49 unique values
0 missing
V9numeric1883 unique values
0 missing
V10numeric29 unique values
0 missing
V11numeric2431 unique values
0 missing
V12numeric219 unique values
0 missing
V13numeric3079 unique values
0 missing
V1numeric1309 unique values
0 missing
V15numeric4674 unique values
0 missing
V16numeric3095 unique values
0 missing
V17numeric1969 unique values
0 missing
V18numeric134 unique values
0 missing
V19numeric3368 unique values
0 missing
V20numeric108 unique values
0 missing
V21numeric3841 unique values
0 missing
V22numeric103 unique values
0 missing
V23numeric4182 unique values
0 missing
V24numeric121 unique values
0 missing
V25numeric4393 unique values
0 missing
V26numeric803 unique values
0 missing
Show all 52 features

107 properties

NumberOfInstances
6118
Number of instances (rows) of the dataset.
NumberOfFeatures
52
Number of attributes (columns) of the dataset.
NumberOfClasses
6
Number of distinct values of the target attribute (if it is nominal).
NumberOfMissingValues
0
Number of missing values in the dataset.
NumberOfInstancesWithMissingValues
0
Number of instances with at least one value missing.
NumberOfNumericFeatures
51
Number of numeric attributes.
NumberOfSymbolicFeatures
1
Number of nominal attributes.
AutoCorrelation
0.37
Average class difference between consecutive instances.
CfsSubsetEval_DecisionStumpAUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.DecisionStump -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_DecisionStumpErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.trees.DecisionStump -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_DecisionStumpKappa
0.35
Kappa coefficient achieved by the landmarker weka.classifiers.trees.DecisionStump -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_NaiveBayesAUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.bayes.NaiveBayes -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_NaiveBayesErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.bayes.NaiveBayes -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_NaiveBayesKappa
0.35
Kappa coefficient achieved by the landmarker weka.classifiers.bayes.NaiveBayes -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_kNN1NAUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.lazy.IBk -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_kNN1NErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.lazy.IBk -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
CfsSubsetEval_kNN1NKappa
0.35
Kappa coefficient achieved by the landmarker weka.classifiers.lazy.IBk -E "weka.attributeSelection.CfsSubsetEval -P 1 -E 1" -S "weka.attributeSelection.BestFirst -D 1 -N 5" -W
ClassEntropy
2.3
Entropy of the target attribute values.
DecisionStumpAUC
0.6
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.DecisionStump
DecisionStumpErrRate
0.58
Error rate achieved by the landmarker weka.classifiers.trees.DecisionStump
DecisionStumpKappa
0
Kappa coefficient achieved by the landmarker weka.classifiers.trees.DecisionStump
Dimensionality
0.01
Number of attributes divided by the number of instances.
EquivalentNumberOfAtts
Number of attributes needed to optimally describe the class (under the assumption of independence among attributes). Equals ClassEntropy divided by MeanMutualInformation.
J48.00001.AUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.J48 -C .00001
J48.00001.ErrRate
0.47
Error rate achieved by the landmarker weka.classifiers.trees.J48 -C .00001
J48.00001.Kappa
0.38
Kappa coefficient achieved by the landmarker weka.classifiers.trees.J48 -C .00001
J48.0001.AUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.J48 -C .0001
J48.0001.ErrRate
0.47
Error rate achieved by the landmarker weka.classifiers.trees.J48 -C .0001
J48.0001.Kappa
0.38
Kappa coefficient achieved by the landmarker weka.classifiers.trees.J48 -C .0001
J48.001.AUC
0.71
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.J48 -C .001
J48.001.ErrRate
0.47
Error rate achieved by the landmarker weka.classifiers.trees.J48 -C .001
J48.001.Kappa
0.38
Kappa coefficient achieved by the landmarker weka.classifiers.trees.J48 -C .001
MajorityClassPercentage
41.75
Percentage of instances belonging to the most frequent class.
MajorityClassSize
2554
Number of instances belonging to the most frequent class.
MaxAttributeEntropy
Maximum entropy among attributes.
MaxKurtosisOfNumericAtts
2944.65
Maximum kurtosis among attributes of the numeric type.
MaxMeansOfNumericAtts
0.05
Maximum of means among attributes of the numeric type.
MaxMutualInformation
Maximum mutual information between the nominal attributes and the target attribute.
MaxNominalAttDistinctValues
6
The maximum number of distinct values among attributes of the nominal type.
MaxSkewnessOfNumericAtts
53.78
Maximum skewness among attributes of the numeric type.
MaxStdDevOfNumericAtts
1.51
Maximum standard deviation of attributes of the numeric type.
MeanAttributeEntropy
Average entropy of the attributes.
MeanKurtosisOfNumericAtts
228.19
Mean kurtosis among attributes of the numeric type.
MeanMeansOfNumericAtts
-0
Mean of means among attributes of the numeric type.
MeanMutualInformation
Average mutual information between the nominal attributes and the target attribute.
MeanNoiseToSignalRatio
An estimate of the amount of irrelevant information in the attributes regarding the class. Equals (MeanAttributeEntropy - MeanMutualInformation) divided by MeanMutualInformation.
MeanNominalAttDistinctValues
6
Average number of distinct values among the attributes of the nominal type.
MeanSkewnessOfNumericAtts
7.44
Mean skewness among attributes of the numeric type.
MeanStdDevOfNumericAtts
0.99
Mean standard deviation of attributes of the numeric type.
MinAttributeEntropy
Minimal entropy among attributes.
MinKurtosisOfNumericAtts
-0.97
Minimum kurtosis among attributes of the numeric type.
MinMeansOfNumericAtts
-0.04
Minimum of means among attributes of the numeric type.
MinMutualInformation
Minimal mutual information between the nominal attributes and the target attribute.
MinNominalAttDistinctValues
6
The minimal number of distinct values among attributes of the nominal type.
MinSkewnessOfNumericAtts
-1.88
Minimum skewness among attributes of the numeric type.
MinStdDevOfNumericAtts
0.84
Minimum standard deviation of attributes of the numeric type.
MinorityClassPercentage
7.94
Percentage of instances belonging to the least frequent class.
MinorityClassSize
486
Number of instances belonging to the least frequent class.
NaiveBayesAUC
0.62
Area Under the ROC Curve achieved by the landmarker weka.classifiers.bayes.NaiveBayes
NaiveBayesErrRate
0.83
Error rate achieved by the landmarker weka.classifiers.bayes.NaiveBayes
NaiveBayesKappa
0.05
Kappa coefficient achieved by the landmarker weka.classifiers.bayes.NaiveBayes
NumberOfBinaryFeatures
0
Number of binary attributes.
PercentageOfBinaryFeatures
0
Percentage of binary attributes.
PercentageOfInstancesWithMissingValues
0
Percentage of instances having missing values.
PercentageOfMissingValues
0
Percentage of missing values.
PercentageOfNumericFeatures
98.08
Percentage of numeric attributes.
PercentageOfSymbolicFeatures
1.92
Percentage of nominal attributes.
Quartile1AttributeEntropy
First quartile of entropy among attributes.
Quartile1KurtosisOfNumericAtts
1.33
First quartile of kurtosis among attributes of the numeric type.
Quartile1MeansOfNumericAtts
-0.01
First quartile of means among attributes of the numeric type.
Quartile1MutualInformation
First quartile of mutual information between the nominal attributes and the target attribute.
Quartile1SkewnessOfNumericAtts
1.33
First quartile of skewness among attributes of the numeric type.
Quartile1StdDevOfNumericAtts
0.97
First quartile of standard deviation of attributes of the numeric type.
Quartile2AttributeEntropy
Second quartile (Median) of entropy among attributes.
Quartile2KurtosisOfNumericAtts
15.29
Second quartile (Median) of kurtosis among attributes of the numeric type.
Quartile2MeansOfNumericAtts
-0
Second quartile (Median) of means among attributes of the numeric type.
Quartile2MutualInformation
Second quartile (Median) of mutual information between the nominal attributes and the target attribute.
Quartile2SkewnessOfNumericAtts
3.14
Second quartile (Median) of skewness among attributes of the numeric type.
Quartile2StdDevOfNumericAtts
1
Second quartile (Median) of standard deviation of attributes of the numeric type.
Quartile3AttributeEntropy
Third quartile of entropy among attributes.
Quartile3KurtosisOfNumericAtts
137.49
Third quartile of kurtosis among attributes of the numeric type.
Quartile3MeansOfNumericAtts
0
Third quartile of means among attributes of the numeric type.
Quartile3MutualInformation
Third quartile of mutual information between the nominal attributes and the target attribute.
Quartile3SkewnessOfNumericAtts
10.45
Third quartile of skewness among attributes of the numeric type.
Quartile3StdDevOfNumericAtts
1
Third quartile of standard deviation of attributes of the numeric type.
REPTreeDepth1AUC
0.75
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.REPTree -L 1
REPTreeDepth1ErrRate
0.51
Error rate achieved by the landmarker weka.classifiers.trees.REPTree -L 1
REPTreeDepth1Kappa
0.3
Kappa coefficient achieved by the landmarker weka.classifiers.trees.REPTree -L 1
REPTreeDepth2AUC
0.75
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.REPTree -L 2
REPTreeDepth2ErrRate
0.51
Error rate achieved by the landmarker weka.classifiers.trees.REPTree -L 2
REPTreeDepth2Kappa
0.3
Kappa coefficient achieved by the landmarker weka.classifiers.trees.REPTree -L 2
REPTreeDepth3AUC
0.75
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.REPTree -L 3
REPTreeDepth3ErrRate
0.51
Error rate achieved by the landmarker weka.classifiers.trees.REPTree -L 3
REPTreeDepth3Kappa
0.3
Kappa coefficient achieved by the landmarker weka.classifiers.trees.REPTree -L 3
RandomTreeDepth1AUC
0.69
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.RandomTree -depth 1
RandomTreeDepth1ErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.trees.RandomTree -depth 1
RandomTreeDepth1Kappa
0.36
Kappa coefficient achieved by the landmarker weka.classifiers.trees.RandomTree -depth 1
RandomTreeDepth2AUC
0.69
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.RandomTree -depth 2
RandomTreeDepth2ErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.trees.RandomTree -depth 2
RandomTreeDepth2Kappa
0.36
Kappa coefficient achieved by the landmarker weka.classifiers.trees.RandomTree -depth 2
RandomTreeDepth3AUC
0.69
Area Under the ROC Curve achieved by the landmarker weka.classifiers.trees.RandomTree -depth 3
RandomTreeDepth3ErrRate
0.49
Error rate achieved by the landmarker weka.classifiers.trees.RandomTree -depth 3
RandomTreeDepth3Kappa
0.36
Kappa coefficient achieved by the landmarker weka.classifiers.trees.RandomTree -depth 3
StdvNominalAttDistinctValues
0
Standard deviation of the number of distinct values among attributes of the nominal type.
kNN1NAUC
0.72
Area Under the ROC Curve achieved by the landmarker weka.classifiers.lazy.IBk
kNN1NErrRate
0.46
Error rate achieved by the landmarker weka.classifiers.lazy.IBk
kNN1NKappa
0.39
Kappa coefficient achieved by the landmarker weka.classifiers.lazy.IBk
Show all 107 properties

45 tasks

Supervised Classification on first-order-theorem-proving
18740 runs - estimation_procedure: 10-fold Crossvalidation - target_feature: Class
Supervised Classification on first-order-theorem-proving
31 runs - estimation_procedure: 10-fold Crossvalidation - target_feature: Class
Supervised Classification on first-order-theorem-proving
1 runs - estimation_procedure: 5 times 2-fold Crossvalidation - target_feature: Class
Supervised Classification on first-order-theorem-proving
0 runs - estimation_procedure: 33% Holdout set - target_feature: Class
Supervised Classification on first-order-theorem-proving
0 runs - estimation_procedure: 10 times 10-fold Crossvalidation - target_feature: Class
Supervised Classification on first-order-theorem-proving
0 runs - estimation_procedure: 33% Holdout set - evaluation_measure: predictive_accuracy - target_feature: Class
Supervised Classification on first-order-theorem-proving
0 runs - estimation_procedure: 10-fold Crossvalidation - evaluation_measure: predictive_accuracy - target_feature: Class
Supervised Classification on first-order-theorem-proving
0 runs - estimation_procedure: 4-fold Crossvalidation - target_feature: Class
Learning Curve on first-order-theorem-proving
43 runs - estimation_procedure: 10-fold Learning Curve - target_feature: Class
Clustering on first-order-theorem-proving
0 runs - target_feature: Class
Clustering on first-order-theorem-proving
0 runs
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Clustering on first-order-theorem-proving
0 runs - estimation_procedure: 50 times Clustering
Subgroup Discovery on first-order-theorem-proving
1312 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
1309 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
1304 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
1303 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
1300 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
1299 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Subgroup Discovery on first-order-theorem-proving
0 runs - target_feature: Class
Define a new task