{"id":"W2058282107","doi":"10.1145/2406336.2406349","title":"Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL","year":2013,"lang":"en","type":"article","venue":"ACM Transactions on Embedded Computing Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Probabilistic logic; Dependability; Theoretical computer science; Automated theorem proving; Measure (data warehouse); Class (philosophy); Artificial intelligence; Programming language; Data mining; Software engineering","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.009168622,0.0009016955,0.001054249,0.002412093,0.001140678,0.003648912,0.002629855,0.001498653,0.003379017],"category_scores_gemma":[0.01472885,0.0006745523,0.003161959,0.001399018,0.008939006,0.007062133,0.004126533,0.00517619,0.0007489027],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002454602,"about_ca_system_score_gemma":0.002472195,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001221187,"about_ca_topic_score_gemma":0.0008891777,"domain_scores_codex":[0.9943305,0.001844457,0.0005158203,0.0005850355,0.002290797,0.0004333776],"domain_scores_gemma":[0.9883701,0.008196875,0.0006282201,0.00147478,0.001094782,0.0002352395],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000007311927,0.00001401077,0.00008313079,0.00005149858,0.0000126035,0.00009630602,0.0001596457,0.004265112,0.0006648678,0.9893988,0.0003198741,0.004926753],"study_design_scores_gemma":[0.00002366866,0.0000364657,0.00009948611,0.00005658016,0.00002163563,0.0001506813,0.00004895587,0.05854067,0.002943145,0.9288545,0.009196225,0.00002790858],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0018351,0.0001276153,0.9953964,0.0003496695,0.00004935493,0.00004069568,0.00003896147,0.0002227245,0.001939534],"genre_scores_gemma":[0.2691917,0.0007823894,0.7236307,0.0009084861,0.0004799053,0.0005989653,0.0002601547,0.000440465,0.00370715],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.009168622,"threshold_uncertainty_score":0.04848891,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02621687487000435,"score_gpt":0.2903207323166397,"score_spread":0.2641038574466353,"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."}}