{"id":"W1525100661","doi":"","title":"The verification of MDG algorithms in the HOL theorem prover","year":2008,"lang":"en","type":"book","venue":"Spectrum Research Repository (Concordia University)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Automated theorem proving; Correctness; Computer science; Theoretical computer science; Programming language; Formal verification; Algorithm","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":"codex-gemma-dda1882f352a","candidate_categories":["open_science"],"consensus_categories":[],"category_scores_codex":[0.003822094,0.0002697863,0.0003250928,0.0007812863,0.000974694,0.0002201574,0.005670924,0.0003309946,0.000002655704],"category_scores_gemma":[0.0002598656,0.0001976823,0.0002062355,0.001508125,0.001401387,0.0005917649,0.0006267392,0.001719552,0.00003045984],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001081222,"about_ca_system_score_gemma":0.001850614,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0009183441,"about_ca_topic_score_gemma":0.0003113792,"domain_scores_codex":[0.9943779,0.00222784,0.0005034202,0.000730997,0.001519272,0.0006405772],"domain_scores_gemma":[0.9953232,0.001227799,0.000456469,0.002515354,0.000374503,0.0001027001],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0001163133,0.00009581115,0.0006792822,0.00006862961,0.00005804515,0.0003210077,0.001392055,0.00001488364,0.0003102942,0.9794836,0.005564028,0.01189606],"study_design_scores_gemma":[0.0007969391,0.0008129677,0.02041685,0.0001791345,0.00003489407,0.0001914715,0.0008146424,0.007657583,0.008076219,0.02544235,0.934881,0.0006959363],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"other","genre_gemma":"other","genre_scores_codex":[0.003229808,0.0004791101,0.01858724,0.0009191105,0.001035403,0.001954127,0.00000955113,0.00010909,0.9736766],"genre_scores_gemma":[0.1317098,0.002315635,0.007063001,0.00004216854,0.0009386571,0.00004686988,0.00002464903,0.00009075734,0.8577685],"genre_candidate":"other","genre_consensus":"other","teacher_disagreement_score":0.9540412,"threshold_uncertainty_score":0.9997089,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0462385237816129,"score_gpt":0.2944333207553769,"score_spread":0.248194796973764,"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."}}