{"id":"W1513403094","doi":"10.1007/978-3-540-30476-0_24","title":"Providing Automated Verification in HOL Using MDGs","year":2004,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Automated theorem proving; Reachability; Computer science; Model checking; Formal verification; Theoretical computer science; Programming language; Automated proof checking; State space; Automation; State (computer science); Formal methods; Equivalence (formal languages); Set (abstract data type); Proof assistant; Algorithm; Mathematical proof; Mathematics; Discrete mathematics","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001882174,0.0004867499,0.0004685231,0.001442116,0.0002221314,0.0005348597,0.003124256,0.0004214627,0.000007350939],"category_scores_gemma":[0.0003392122,0.0005018854,0.0000850575,0.00140873,0.0004842753,0.001431916,0.0007718914,0.0008327821,0.00003028067],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001597565,"about_ca_system_score_gemma":0.001102457,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00008430456,"about_ca_topic_score_gemma":0.0000252552,"domain_scores_codex":[0.9959241,0.00008065916,0.0007793574,0.001605019,0.0009326046,0.0006783119],"domain_scores_gemma":[0.9973481,0.0001756127,0.0004851081,0.0015698,0.0002993605,0.0001219901],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001038623,0.00006370273,0.0001121596,0.0001288618,0.000007649323,0.0000731507,0.002143591,0.3900213,0.005006944,0.1209663,0.000003381234,0.4814625],"study_design_scores_gemma":[0.0002044263,0.00006733676,0.0003579329,0.0005937585,0.000003881416,0.0000414609,1.818171e-7,0.9221352,0.008000014,0.06797308,0.00009985823,0.0005229153],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0008727915,0.0001775438,0.9946303,0.0001623805,0.002086273,0.0006580043,0.000001966929,0.0005479523,0.0008627507],"genre_scores_gemma":[0.1459601,0.00001549592,0.8534901,0.0002801619,0.0001802897,0.00001225561,0.000003841251,0.00003210307,0.00002575823],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.5321139,"threshold_uncertainty_score":0.9997433,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04216792123757171,"score_gpt":0.3063406616379988,"score_spread":0.264172740400427,"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."}}