DEVELOPMENT... { "data_id": "1475", "name": "first-order-theorem-proving", "exact_name": "first-order-theorem-proving", "version": 1, "version_label": null, "description": "**Author**: James P Bridge, Sean B Holden and Lawrence C Paulson \r\n \r\n**Source**: [UCI](https:\/\/archive.ics.uci.edu\/ml\/datasets\/First-order+theorem+proving) \r\n\r\n**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. \r\n\r\nSource:\r\n\r\nJames P Bridge, Sean B Holden and Lawrence C Paulson \r\n\r\nUniversity of Cambridge \r\nComputer Laboratory \r\nWilliam Gates Building \r\n15 JJ Thomson Avenue \r\nCambridge CB3 0FD \r\nUK \r\n\r\n+44 (0)1223 763500 \r\nforename.surname '@' cl.cam.ac.uk\r\n\r\n\r\nData Set Information:\r\n\r\nSee the file dataset file.\r\n\r\n\r\nAttribute Information:\r\n\r\nThe attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details.\r\n", "format": "ARFF", "uploader": "unknown", "uploader_id": 64, "visibility": "public", "creator": null, "contributor": null, "date": "2015-05-22 17:30:40", "update_comment": null, "last_update": "2015-11-09 20:36:55", "licence": "Public", "status": "active", "error_message": null, "url": "https:\/\/www.openml.org\/data\/download\/1587932\/phpPbCMyg", "default_target_attribute": "Class", "row_id_attribute": null, "ignore_attribute": null, "runs": 26642, "suggest": { "input": [ "first-order-theorem-proving", "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. " ], "weight": 5 }, "qualities": { "NumberOfInstances": 6118, "NumberOfFeatures": 52, "NumberOfClasses": 6, "NumberOfMissingValues": 0, "NumberOfInstancesWithMissingValues": 0, "NumberOfNumericFeatures": 51, "NumberOfSymbolicFeatures": 1, "AutoCorrelation": 0.3678273663560569, "CfsSubsetEval_DecisionStumpAUC": 0.7090827191037619, "CfsSubsetEval_DecisionStumpErrRate": 0.4851258581235698, "CfsSubsetEval_DecisionStumpKappa": 0.346242749551416, "CfsSubsetEval_NaiveBayesAUC": 0.7090827191037619, "CfsSubsetEval_NaiveBayesErrRate": 0.4851258581235698, "CfsSubsetEval_NaiveBayesKappa": 0.346242749551416, "CfsSubsetEval_kNN1NAUC": 0.7090827191037619, "CfsSubsetEval_kNN1NErrRate": 0.4851258581235698, "CfsSubsetEval_kNN1NKappa": 0.346242749551416, "ClassEntropy": 2.3000070580673455, "DecisionStumpAUC": 0.5958041430205936, "DecisionStumpErrRate": 0.582543314808761, "DecisionStumpKappa": 0, "Dimensionality": 0.008499509643674403, "EquivalentNumberOfAtts": null, "J48.00001.AUC": 0.7129106639983, "J48.00001.ErrRate": 0.465675057208238, "J48.00001.Kappa": 0.375395542857667, "J48.0001.AUC": 0.7129106639983, "J48.0001.ErrRate": 0.465675057208238, "J48.0001.Kappa": 0.375395542857667, "J48.001.AUC": 0.7129106639983, "J48.001.ErrRate": 0.465675057208238, "J48.001.Kappa": 0.375395542857667, "MajorityClassPercentage": 41.745668519123896, "MajorityClassSize": 2554, "MaxAttributeEntropy": null, "MaxKurtosisOfNumericAtts": 2944.6525317078385, "MaxMeansOfNumericAtts": 0.052954623733246275, "MaxMutualInformation": null, "MaxNominalAttDistinctValues": 6, "MaxSkewnessOfNumericAtts": 53.784844915558836, "MaxStdDevOfNumericAtts": 1.5063662920278478, "MeanAttributeEntropy": null, "MeanKurtosisOfNumericAtts": 228.1908672595734, "MeanMeansOfNumericAtts": -0.0005510331198841205, "MeanMutualInformation": null, "MeanNoiseToSignalRatio": null, "MeanNominalAttDistinctValues": 6, "MeanSkewnessOfNumericAtts": 7.440976027873651, "MeanStdDevOfNumericAtts": 0.9916438519187979, "MinAttributeEntropy": null, "MinKurtosisOfNumericAtts": -0.971971602375862, "MinMeansOfNumericAtts": -0.04091056701536289, "MinMutualInformation": null, "MinNominalAttDistinctValues": 6, "MinSkewnessOfNumericAtts": -1.875764427110436, "MinStdDevOfNumericAtts": 0.8394622129143448, "MinorityClassPercentage": 7.943772474664923, "MinorityClassSize": 486, "NaiveBayesAUC": 0.620496665896741, "NaiveBayesErrRate": 0.8345864661654135, "NaiveBayesKappa": 0.05473977746349635, "NumberOfBinaryFeatures": 0, "PercentageOfBinaryFeatures": 0, "PercentageOfInstancesWithMissingValues": 0, "PercentageOfMissingValues": 0, "PercentageOfNumericFeatures": 98.07692307692307, "PercentageOfSymbolicFeatures": 1.9230769230769231, "Quartile1AttributeEntropy": null, "Quartile1KurtosisOfNumericAtts": 1.3326773975344213, "Quartile1MeansOfNumericAtts": -0.0081597994442654, "Quartile1MutualInformation": null, "Quartile1SkewnessOfNumericAtts": 1.3330441633458074, "Quartile1StdDevOfNumericAtts": 0.9727856745152441, "Quartile2AttributeEntropy": null, "Quartile2KurtosisOfNumericAtts": 15.286501444565163, "Quartile2MeansOfNumericAtts": -0.002469232265446736, "Quartile2MutualInformation": null, "Quartile2SkewnessOfNumericAtts": 3.1426279908840025, "Quartile2StdDevOfNumericAtts": 0.99719270235299, "Quartile3AttributeEntropy": null, "Quartile3KurtosisOfNumericAtts": 137.49118065052153, "Quartile3MeansOfNumericAtts": 0.002845900948022519, "Quartile3MutualInformation": null, "Quartile3SkewnessOfNumericAtts": 10.454373740045988, "Quartile3StdDevOfNumericAtts": 1.0036680416341404, "REPTreeDepth1AUC": 0.7474597786162569, "REPTreeDepth1ErrRate": 0.5052304674730304, "REPTreeDepth1Kappa": 0.3022006426588284, "REPTreeDepth2AUC": 0.7474597786162569, "REPTreeDepth2ErrRate": 0.5052304674730304, "REPTreeDepth2Kappa": 0.3022006426588284, "REPTreeDepth3AUC": 0.7474597786162569, "REPTreeDepth3ErrRate": 0.5052304674730304, "REPTreeDepth3Kappa": 0.3022006426588284, "RandomTreeDepth1AUC": 0.6943273232081051, "RandomTreeDepth1ErrRate": 0.4870872834259562, "RandomTreeDepth1Kappa": 0.3568830760926545, "RandomTreeDepth2AUC": 0.6943273232081051, "RandomTreeDepth2ErrRate": 0.4870872834259562, "RandomTreeDepth2Kappa": 0.3568830760926545, "RandomTreeDepth3AUC": 0.6943273232081051, "RandomTreeDepth3ErrRate": 0.4870872834259562, "RandomTreeDepth3Kappa": 0.3568830760926545, "StdvNominalAttDistinctValues": 0, "kNN1NAUC": 0.716082344973639, "kNN1NErrRate": 0.4635501797973194, "kNN1NKappa": 0.3867635866819356 }, "tags": [ { "tag": "OpenML-CC18", "uploader": "1" }, { "tag": "OpenML100", "uploader": "348" }, { "tag": "study_123", "uploader": "3886" }, { "tag": "study_14", "uploader": "64" }, { "tag": "study_34", "uploader": "1" }, { "tag": "study_50", "uploader": "64" }, { "tag": "study_52", "uploader": "64" }, { "tag": "study_7", "uploader": "64" }, { "tag": "study_98", "uploader": "1935" }, { "tag": "study_99", "uploader": "1" }, { "tag": "study_225", "uploader": "0" }, { "tag": "study_236", "uploader": "0" }, { "tag": "study_293", "uploader": "0" }, { "tag": "study_270", "uploader": "0" }, { "tag": "study_271", "uploader": "0" }, { "tag": "study_253", "uploader": "0" }, { "tag": "study_282", "uploader": "0" }, { "tag": "study_275", "uploader": "0" } ], "features": [ { "name": "Class", "index": "51", "type": "nominal", "distinct": "6", "missing": "0", "target": "1", "distr": [ [ "1", "2", "3", "4", "5", "6" ], [ [ "1089", "0", "0", "0", "0", "0" ], [ "0", "486", "0", "0", "0", "0" ], [ "0", "0", "748", "0", "0", "0" ], [ "0", "0", "0", "617", "0", "0" ], [ "0", "0", "0", "0", "624", "0" ], [ "0", "0", "0", "0", "0", "2554" ] ] ] }, { "name": "V28", "index": "27", "type": "numeric", "distinct": "1023", "missing": "0", "min": "0", "max": "28", "mean": "0", "stdev": "1" }, { "name": "V27", "index": "26", "type": "numeric", "distinct": "4560", "missing": "0", "min": "-2", "max": "13", "mean": "0", "stdev": "1" }, { "name": "V29", "index": "28", "type": "numeric", "distinct": "4709", "missing": "0", "min": "-1", "max": "29", "mean": "0", "stdev": "1" }, { "name": "V30", "index": "29", "type": "numeric", "distinct": "69", "missing": "0", "min": "0", "max": "7", "mean": "0", "stdev": "1" }, { "name": "V31", "index": "30", "type": "numeric", "distinct": "79", "missing": "0", "min": "-1", "max": "5", "mean": "0", "stdev": "1" }, { "name": "V32", "index": "31", "type": "numeric", "distinct": "82", "missing": "0", "min": "-3", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V33", "index": "32", "type": "numeric", "distinct": "23", "missing": "0", "min": "0", "max": "55", "mean": "0", "stdev": "1" }, { "name": "V34", "index": "33", "type": "numeric", "distinct": "31", "missing": "0", "min": "0", "max": "16", "mean": "0", "stdev": "1" }, { "name": "V35", "index": "34", "type": "numeric", "distinct": "48", "missing": "0", "min": "0", "max": "10", "mean": "0", "stdev": "1" }, { "name": "V36", "index": "35", "type": "numeric", "distinct": "70", "missing": "0", "min": "0", "max": "68", "mean": "0", "stdev": "2" }, { "name": "V37", "index": "36", "type": "numeric", "distinct": "1053", "missing": "0", "min": "0", "max": "15", "mean": "0", "stdev": "1" }, { "name": "V38", "index": "37", "type": "numeric", "distinct": "1569", "missing": "0", "min": "-1", "max": "16", "mean": "0", "stdev": "1" }, { "name": "V39", "index": "38", "type": "numeric", "distinct": "893", "missing": "0", "min": "0", "max": "16", "mean": "0", "stdev": "1" }, { "name": "V40", "index": "39", "type": "numeric", "distinct": "72", "missing": "0", "min": "0", "max": "29", "mean": "0", "stdev": "1" }, { "name": "V41", "index": "40", "type": "numeric", "distinct": "1041", "missing": "0", "min": "0", "max": "15", "mean": "0", "stdev": "1" }, { "name": "V42", "index": "41", "type": "numeric", "distinct": "37", "missing": "0", "min": "0", "max": "31", "mean": "0", "stdev": "1" }, { "name": "V43", "index": "42", "type": "numeric", "distinct": "29", "missing": "0", "min": "0", "max": "54", "mean": "0", "stdev": "1" }, { "name": "V44", "index": "43", "type": "numeric", "distinct": "1698", "missing": "0", "min": "-1", "max": "2", "mean": "0", "stdev": "1" }, { "name": "V45", "index": "44", "type": "numeric", "distinct": "2246", "missing": "0", "min": "-2", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V46", "index": "45", "type": "numeric", "distinct": "1941", "missing": "0", "min": "-1", "max": "3", "mean": "0", "stdev": "1" }, { "name": "V47", "index": "46", "type": "numeric", "distinct": "1676", "missing": "0", "min": "-1", "max": "2", "mean": "0", "stdev": "1" }, { "name": "V48", "index": "47", "type": "numeric", "distinct": "1703", "missing": "0", "min": "0", "max": "3", "mean": "0", "stdev": "1" }, { "name": "V49", "index": "48", "type": "numeric", "distinct": "2315", "missing": "0", "min": "-1", "max": "2", "mean": "0", "stdev": "1" }, { "name": "V50", "index": "49", "type": "numeric", "distinct": "1537", "missing": "0", "min": "0", "max": "10", "mean": "0", "stdev": "1" }, { "name": "V51", "index": "50", "type": "numeric", "distinct": "2462", "missing": "0", "min": "-2", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V14", "index": "13", "type": "numeric", "distinct": "82", "missing": "0", "min": "-3", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V2", "index": "1", "type": "numeric", "distinct": "1194", "missing": "0", "min": "-4", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V3", "index": "2", "type": "numeric", "distinct": "1148", "missing": "0", "min": "-1", "max": "3", "mean": "0", "stdev": "1" }, { "name": "V4", "index": "3", "type": "numeric", "distinct": "1261", "missing": "0", "min": "-1", "max": "3", "mean": "0", "stdev": "1" }, { "name": "V5", "index": "4", "type": "numeric", "distinct": "1394", "missing": "0", "min": "-1", "max": "2", "mean": "0", "stdev": "1" }, { "name": "V6", "index": "5", "type": "numeric", "distinct": "1030", "missing": "0", "min": "-1", "max": "7", "mean": "0", "stdev": "1" }, { "name": "V7", "index": "6", "type": "numeric", "distinct": "1309", "missing": "0", "min": "-2", "max": "1", "mean": "0", "stdev": "1" }, { "name": "V8", "index": "7", "type": "numeric", "distinct": "49", "missing": "0", "min": "-1", "max": "32", "mean": "0", "stdev": "1" }, { "name": "V9", "index": "8", "type": "numeric", "distinct": "1883", "missing": "0", "min": "-1", "max": "15", "mean": "0", "stdev": "1" }, { "name": "V10", "index": "9", "type": "numeric", "distinct": "29", "missing": "0", "min": "-1", "max": "11", "mean": "0", "stdev": "1" }, { "name": "V11", "index": "10", "type": "numeric", "distinct": "2431", "missing": "0", "min": "-2", "max": "9", "mean": "0", "stdev": "1" }, { "name": "V12", "index": "11", "type": "numeric", "distinct": "219", "missing": "0", "min": "0", "max": "42", "mean": "0", "stdev": "1" }, { "name": "V13", "index": "12", "type": "numeric", "distinct": "3079", "missing": "0", "min": "-1", "max": "23", "mean": "0", "stdev": "1" }, { "name": "V1", "index": "0", "type": "numeric", "distinct": "1309", "missing": "0", "min": "-1", "max": "2", "mean": "0", "stdev": "1" }, { "name": "V15", "index": "14", "type": "numeric", "distinct": "4674", "missing": "0", "min": "0", "max": "31", "mean": "0", "stdev": "1" }, { "name": "V16", "index": "15", "type": "numeric", "distinct": "3095", "missing": "0", "min": "-2", "max": "4", "mean": "0", "stdev": "1" }, { "name": "V17", "index": "16", "type": "numeric", "distinct": "1969", "missing": "0", "min": "0", "max": "18", "mean": "0", "stdev": "1" }, { "name": "V18", "index": "17", "type": "numeric", "distinct": "134", "missing": "0", "min": "-2", "max": "6", "mean": "0", "stdev": "1" }, { "name": "V19", "index": "18", "type": "numeric", "distinct": "3368", "missing": "0", "min": "-3", "max": "10", "mean": "0", "stdev": "1" }, { "name": "V20", "index": "19", "type": "numeric", "distinct": "108", "missing": "0", "min": "-3", "max": "13", "mean": "0", "stdev": "1" }, { "name": "V21", "index": "20", "type": "numeric", "distinct": "3841", "missing": "0", "min": "-2", "max": "37", "mean": "0", "stdev": "1" }, { "name": "V22", "index": "21", "type": "numeric", "distinct": "103", "missing": "0", "min": "-2", "max": "14", "mean": "0", "stdev": "1" }, { "name": "V23", "index": "22", "type": "numeric", "distinct": "4182", "missing": "0", "min": "-3", "max": "8", "mean": "0", "stdev": "1" }, { "name": "V24", "index": "23", "type": "numeric", "distinct": "121", "missing": "0", "min": "-2", "max": "10", "mean": "0", "stdev": "1" }, { "name": "V25", "index": "24", "type": "numeric", "distinct": "4393", "missing": "0", "min": "-2", "max": "9", "mean": "0", "stdev": "1" }, { "name": "V26", "index": "25", "type": "numeric", "distinct": "803", "missing": "0", "min": "-1", "max": "15", "mean": "0", "stdev": "1" } ], "nr_of_issues": 0, "nr_of_downvotes": 0, "nr_of_likes": 0, "nr_of_downloads": 0, "total_downloads": 0, "reach": 0, "reuse": 0, "impact_of_reuse": 0, "reach_of_reuse": 0, "impact": 0 }