{"id":"W7015220610","doi":"","title":"Semi-Automation of Meta-Theoretic Proofs","year":2023,"lang":"en","type":"dissertation","venue":"eScholarship@McGill (McGill)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Natural deduction; Sequent calculus; Gas meter prover; Soundness; Calculus (dental); Automated theorem proving; Automated proof checking; Curry–Howard correspondence","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.007895659,0.0007279231,0.0009359863,0.001528223,0.001011429,0.002829278,0.002878945,0.0008312727,0.00624125],"category_scores_gemma":[0.03214351,0.001486484,0.002238588,0.0007137185,0.002689241,0.003551287,0.005623009,0.002787822,0.002533213],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001275446,"about_ca_system_score_gemma":0.002679029,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001379354,"about_ca_topic_score_gemma":0.002271401,"domain_scores_codex":[0.9874955,0.005497854,0.0007399123,0.001295919,0.00428162,0.0006892418],"domain_scores_gemma":[0.9566915,0.02870109,0.001222997,0.009439238,0.003483534,0.0004615913],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0007144822,0.0003655406,0.002521099,0.001374419,0.0002470144,0.0009220956,0.004578704,0.05761868,0.1033979,0.3989539,0.008423829,0.4208824],"study_design_scores_gemma":[0.0002472435,0.0002592814,0.001333786,0.0003032132,0.0001341601,0.0006813285,0.0004036726,0.470568,0.1061319,0.3705339,0.04926636,0.0001372411],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01390843,0.000119556,0.9742915,0.0002003129,0.00003150248,0.0001293351,0.0001189772,0.007588248,0.003612188],"genre_scores_gemma":[0.2432826,0.0001807833,0.751833,0.0001813367,0.00004533801,0.0001941,0.0004125238,0.001298303,0.002571922],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007895659,"threshold_uncertainty_score":0.04175675,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02973873265478744,"score_gpt":0.2580544613430447,"score_spread":0.2283157286882573,"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."}}