{"id":"W1605983610","doi":"","title":"Theorem proving in higher order logics : 21st international conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008, proceedings","year":2008,"lang":"en","type":"book","venue":"Springer eBooks","topic":"Logic, Reasoning, and Knowledge","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":false,"ca_institutions":"","funders":"","keywords":"HOL; Automated theorem proving; Computer science; Proof assistant; Programming language; Automated proof checking; Mathematical proof; Soundness; Theoretical computer science; Calculus (dental); Discrete mathematics; Mathematics","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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.0003394565,0.000803508,0.00077198,0.0004323961,0.000228998,0.0004654034,0.002778673,0.0005754945,0.0004318823],"category_scores_gemma":[0.00008166465,0.000734729,0.0001630114,0.0001698112,0.0002705078,0.0003106679,0.001025926,0.001146815,0.00009142278],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001185696,"about_ca_system_score_gemma":0.005097566,"about_ca_topic_candidate":true,"about_ca_topic_consensus":true,"about_ca_topic_score_codex":0.04042055,"about_ca_topic_score_gemma":0.1652737,"domain_scores_codex":[0.995943,0.00003876884,0.0007569104,0.001329359,0.0009772731,0.000954722],"domain_scores_gemma":[0.9975923,0.00008989923,0.0005516893,0.0006499348,0.0008197809,0.0002963424],"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.00003305,0.0001088231,0.001378269,0.000137329,0.0001626443,0.0005356437,0.001362736,0.000009402408,0.00004238581,0.6273658,0.3547266,0.01413729],"study_design_scores_gemma":[0.001163066,0.00009871741,0.005032126,0.0006269722,0.00003560755,0.0001121486,0.0000569242,0.001402982,0.0001410203,0.02169726,0.9679664,0.001666812],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"other","genre_gemma":"other","genre_scores_codex":[0.0002830927,0.000444464,0.0004239154,0.0001916175,0.002151444,0.000714886,0.00002657691,0.0003608394,0.9954032],"genre_scores_gemma":[0.03236616,0.0001348264,0.001696441,0.0004308918,0.0009580171,0.0001190207,0.00002673498,0.0001135083,0.9641544],"genre_candidate":"other","genre_consensus":"other","teacher_disagreement_score":0.6132398,"threshold_uncertainty_score":0.9995103,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03024942183449027,"score_gpt":0.2244565025360769,"score_spread":0.1942070807015866,"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."}}