{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0056073,0.001186003,0.001591236,0.001914579,0.001402871,0.007234767,0.002990196,0.000932932,0.04048822],"category_scores_gemma":[0.00498006,0.001264802,0.001500618,0.00415097,0.003078586,0.006129784,0.002080638,0.002996965,0.00595976],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.01081435,"about_ca_system_score_gemma":0.01518093,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.102929,"about_ca_topic_score_gemma":0.1097848,"domain_scores_codex":[0.9980755,0.0003486483,0.0001125955,0.0003224999,0.0009673627,0.0001735031],"domain_scores_gemma":[0.995528,0.002089316,0.0001230625,0.0006569206,0.001298237,0.0003044128],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"not_applicable","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0001564883,0.0001624568,0.0005436334,0.0007396193,0.00007373026,0.0001105725,0.000393349,0.004523169,0.002354402,0.08190124,0.478468,0.4305734],"study_design_scores_gemma":[0.000133036,0.00008201844,0.002275276,0.0008450029,0.0001109924,0.0004190964,0.0003413754,0.04585135,0.005367162,0.1529438,0.7915587,0.00007218889],"study_design_candidate":"not_applicable","study_design_consensus":"not_applicable","genre_codex":"methods","genre_gemma":"other","genre_scores_codex":[0.01101709,0.1163652,0.7144484,0.01871219,0.008138785,0.0003684949,0.003231558,0.01578555,0.1119328],"genre_scores_gemma":[0.0771362,0.09928994,0.5215978,0.002917191,0.004519014,0.0003805005,0.01373722,0.004978003,0.2754441],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.102929,"threshold_uncertainty_score":0.2046598,"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."}}