{"id":"W2887657530","doi":"10.1017/s0960129518000154","title":"Mechanizing proofs with logical relations – Kripke-style","year":2018,"lang":"en","type":"article","venue":"Mathematical Structures in Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Computer science; Normalization (sociology); Logical consequence; Theoretical computer science; Programming language; Algebra over a field; Calculus (dental); Mathematics; Artificial intelligence; Pure 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":[],"consensus_categories":[],"category_scores_codex":[0.0008472812,0.0002054853,0.0002507447,0.0001980975,0.0004070433,0.0006122121,0.00188547,0.00007012564,0.00005356515],"category_scores_gemma":[0.0001017452,0.0001299896,0.00004018531,0.001442724,0.0008047794,0.0006314199,0.000704371,0.0002032605,0.0001126567],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008884944,"about_ca_system_score_gemma":0.0001212821,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008080292,"about_ca_topic_score_gemma":0.00001466111,"domain_scores_codex":[0.9974794,0.00006381067,0.0003503501,0.0007505107,0.0007596092,0.0005963185],"domain_scores_gemma":[0.9986338,0.0001314658,0.0001141728,0.0007611506,0.0001769527,0.0001824686],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000002538776,0.00004323271,0.0004649899,0.00001444874,0.000002964425,0.00002319556,0.001113099,0.00007019957,0.00008867513,0.9697729,0.00005829963,0.02834544],"study_design_scores_gemma":[0.000228513,0.0002440432,0.002029753,0.00001777308,0.000002683441,0.0002063052,0.0000151723,0.2975844,0.000726032,0.6981961,0.0005042969,0.0002449461],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.008049759,0.00002046584,0.9861128,0.0002728684,0.0004318651,0.0003244895,1.844195e-7,0.0002165281,0.00457099],"genre_scores_gemma":[0.6857498,1.696786e-7,0.3139088,0.0001494803,0.0001374459,0.00001232533,2.252813e-7,0.000005572071,0.00003617215],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6777,"threshold_uncertainty_score":0.5903575,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02551804787441153,"score_gpt":0.263819457371371,"score_spread":0.2383014094969594,"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."}}