{"id":"W2090121147","doi":"10.1016/j.entcs.2004.01.021","title":"Probabilistic Guarded Commands Mechanized in HOL","year":2005,"lang":"en","type":"article","venue":"Electronic Notes in Theoretical Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":17,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"University of Sydney; Macquarie University; Magdalen College, University of Oxford","keywords":"HOL; Correctness; Computer science; Probabilistic logic; Predicate transformer semantics; Automated theorem proving; Mutual exclusion; Proof assistant; Programming language; Theoretical computer science; Mathematical proof; Algorithm; Operational semantics; Artificial intelligence; Mathematics; Semantics (computer science)","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001761087,0.0005278793,0.0004843622,0.0009501808,0.0008654473,0.002246562,0.002162281,0.0008236552,0.007198833],"category_scores_gemma":[0.004489985,0.0007779719,0.001201174,0.0005768883,0.004127623,0.004978352,0.003745527,0.003059301,0.001283301],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001306913,"about_ca_system_score_gemma":0.001744719,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002076194,"about_ca_topic_score_gemma":0.002684314,"domain_scores_codex":[0.9979367,0.0004779499,0.0001307701,0.0002945441,0.0008443558,0.0003157012],"domain_scores_gemma":[0.9965959,0.001579023,0.0001974218,0.001186863,0.000353245,0.00008750235],"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.0001395727,0.00009123918,0.0005193422,0.0002298564,0.0000250764,0.0004393483,0.0006717109,0.02575502,0.01026305,0.9200235,0.005384379,0.03645788],"study_design_scores_gemma":[0.0001589597,0.00009424755,0.0002847512,0.000126521,0.00006230547,0.0002944687,0.000138686,0.1396322,0.0415876,0.7618075,0.05573608,0.00007667681],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01484019,0.0003106829,0.9540645,0.0009846172,0.0002702776,0.0001368615,0.0003020397,0.008269206,0.02082165],"genre_scores_gemma":[0.503213,0.000628943,0.4710033,0.001031086,0.0002813723,0.0004865518,0.000754483,0.002029439,0.02057175],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007198833,"threshold_uncertainty_score":0.02408254,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.00939515989005353,"score_gpt":0.2485082263884564,"score_spread":0.2391130664984029,"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."}}