{"id":"W1972387650","doi":"10.1016/j.jal.2011.01.001","title":"Reasoning about conditional probabilities in a higher-order-logic theorem prover","year":2011,"lang":"en","type":"article","venue":"Journal of Applied Logic","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":12,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Conditional probability; Automated theorem proving; Probabilistic logic; Bayes' theorem; Law of total probability; Theoretical computer science; Computer science; Mathematics; Conditional mutual information; Probability theory; Discrete mathematics; Gas meter prover; Regular conditional probability; Algorithm; Posterior probability; Artificial intelligence; Bayesian probability; Mathematical proof; Programming language; Statistics","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.0125127,0.001177319,0.001858018,0.002812303,0.001881607,0.005779617,0.004718436,0.002280793,0.009558126],"category_scores_gemma":[0.04021635,0.001800843,0.004284343,0.001827057,0.003819821,0.01103124,0.005219663,0.004123592,0.001420564],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002509954,"about_ca_system_score_gemma":0.003115032,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003107835,"about_ca_topic_score_gemma":0.004815563,"domain_scores_codex":[0.9902501,0.003438858,0.0008616985,0.001345867,0.003212903,0.0008906021],"domain_scores_gemma":[0.9427005,0.05071985,0.001261835,0.002946523,0.001881002,0.0004904127],"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.0003902619,0.000240689,0.003202066,0.0005168598,0.0003102198,0.001089103,0.0007353919,0.07271471,0.006021401,0.8548964,0.004148277,0.05573453],"study_design_scores_gemma":[0.000135699,0.00003765623,0.0002235532,0.00003638979,0.0001554377,0.0002206465,0.00005809673,0.3458413,0.01061056,0.6399473,0.002689531,0.00004377203],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01246573,0.00005156574,0.982599,0.0004253383,0.00005618882,0.00006570756,0.0002025607,0.002289894,0.001843945],"genre_scores_gemma":[0.3950545,0.000191154,0.6001292,0.0005576871,0.0001983464,0.0001218168,0.0006091546,0.0006088558,0.002529226],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.0125127,"threshold_uncertainty_score":0.06617427,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06770647973216208,"score_gpt":0.2773710722070462,"score_spread":0.2096645924748841,"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."}}