{"id":"W3213158637","doi":"10.1017/s0960129521000323","title":"A focused linear logical framework and its application to metatheory of object logics","year":2021,"lang":"en","type":"article","venue":"Mathematical Structures in Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Metatheory; Natural deduction; Sequent calculus; Completeness (order theory); Computer science; Linear logic; Rule of inference; Sequent; Proof calculus; Cut-elimination theorem; Programming language; First-order logic; Theoretical computer science; Concurrency; Inference; Mathematics; Algorithm; Mathematical proof; Artificial intelligence","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.0009490115,0.0001617053,0.000341561,0.0001321182,0.0001061998,0.0001740086,0.001156771,0.00008753269,0.00001052584],"category_scores_gemma":[0.0004910773,0.0001175026,0.00005217544,0.001332992,0.0002308951,0.0002071834,0.000964219,0.0001771361,0.00001447995],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003335297,"about_ca_system_score_gemma":0.0000949126,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000002450624,"about_ca_topic_score_gemma":0.000001924446,"domain_scores_codex":[0.9979157,0.0001015521,0.00040195,0.0006768771,0.0005487177,0.0003551584],"domain_scores_gemma":[0.9985212,0.0003942233,0.0001039998,0.0006181191,0.0001851049,0.0001773248],"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.000002120582,0.00005036132,0.000146398,0.0000525223,0.000003189756,0.00001621198,0.0008358773,0.0003833913,0.0006976723,0.9504079,0.000002753722,0.04740155],"study_design_scores_gemma":[0.0001000523,0.00006683944,0.001561596,0.00001394828,0.000002776216,0.00005233387,0.00001001262,0.2317313,0.004946985,0.7613017,0.00007746443,0.0001350202],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03315377,0.0001612575,0.9656466,0.0002395279,0.00020652,0.0002872021,4.861323e-7,0.00006283438,0.0002417783],"genre_scores_gemma":[0.65139,0.000001896459,0.348327,0.0002178239,0.00004400408,0.00001202294,2.132597e-7,0.00000334481,0.000003778316],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6182362,"threshold_uncertainty_score":0.4791615,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02602241376037715,"score_gpt":0.2903041255594583,"score_spread":0.2642817117990811,"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."}}