{"id":"W2074047803","doi":"10.1007/s11390-010-9407-0","title":"Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving","year":2010,"lang":"en","type":"article","venue":"Journal of Computer Science and Technology","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Probabilistic analysis of algorithms; Mathematical proof; Theory of computation; Computational complexity theory; Algorithm; Automated theorem proving; Probabilistic logic; Time complexity; Descriptive complexity theory; Theoretical computer science; Mathematics; Artificial intelligence","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.01604955,0.002066412,0.002108012,0.003335387,0.00150975,0.008651337,0.006293261,0.002554512,0.006473931],"category_scores_gemma":[0.1116745,0.001880905,0.00357656,0.003376046,0.005165645,0.0170164,0.003706661,0.005157523,0.0004244227],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.005875482,"about_ca_system_score_gemma":0.007278106,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006749988,"about_ca_topic_score_gemma":0.005423663,"domain_scores_codex":[0.9804645,0.006855676,0.001293446,0.00226998,0.005608548,0.003507903],"domain_scores_gemma":[0.6875464,0.2913204,0.006777693,0.008248334,0.00426553,0.001841682],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0009226628,0.0008302806,0.009942908,0.0004557092,0.0003998052,0.0002295617,0.0004262391,0.708617,0.004433843,0.2257523,0.001788204,0.04620139],"study_design_scores_gemma":[0.0001080789,0.000102951,0.0008456679,0.00002358395,0.0001026165,0.00007032613,0.00005947976,0.8531631,0.002730955,0.1423853,0.0003770639,0.00003086311],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2367052,0.0007273894,0.7509658,0.001571686,0.0000940102,0.0002574542,0.0005225123,0.001609671,0.007546358],"genre_scores_gemma":[0.8299691,0.0003204107,0.166609,0.0001875136,0.0001871541,0.0001680015,0.0007475308,0.0004092745,0.001401985],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01604955,"threshold_uncertainty_score":0.08487916,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01665396761359184,"score_gpt":0.2521595947787549,"score_spread":0.235505627165163,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}