{"id":"W2345246322","doi":"10.18778/0138-0680.44.3.4.03","title":"A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics","year":2015,"lang":"en","type":"article","venue":"Bulletin of the Section of Logic","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Mathematical proof; Modal logic; Mathematics; Proof theory; Modal; Normal modal logic; Structural proof theory; Extension (predicate logic); Calculus (dental); Algebra over a field; Discrete mathematics; Proof complexity; Order (exchange); Pure mathematics; Computer science; Programming language","routes":{"ca_aff":false,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0008542308,0.00008398906,0.0001845157,0.00004947087,0.00005840991,0.00001527638,0.0003073758,0.00006869504,0.000006745857],"category_scores_gemma":[0.0002418944,0.00005591194,0.00006397659,0.0001418609,0.00008413135,0.0000381256,0.0001312185,0.00005216275,0.000001020803],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002818038,"about_ca_system_score_gemma":0.00003819507,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001952164,"about_ca_topic_score_gemma":0.00003662129,"domain_scores_codex":[0.9990971,0.00006563775,0.000273184,0.0001805762,0.000266317,0.0001171608],"domain_scores_gemma":[0.9988288,0.00007129521,0.0002428449,0.0002716289,0.0005541479,0.00003127452],"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.0004502377,0.001442093,0.006625921,0.001606302,0.0002084088,0.000002616833,0.004315561,0.01676674,0.003187545,0.877414,0.04441936,0.04356124],"study_design_scores_gemma":[0.005711627,0.007782661,0.006844943,0.0001508833,0.0002024868,0.0002313292,0.001187043,0.09659453,0.1217393,0.3154329,0.4430658,0.001056508],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02675241,0.0006069774,0.9559663,0.003908476,0.001361255,0.001466509,0.000003590281,0.00007431648,0.009860178],"genre_scores_gemma":[0.9921037,0.000004894564,0.007001707,0.00004274388,0.00005916238,0.00002646971,0.000001079974,0.000004679942,0.0007555664],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9653513,"threshold_uncertainty_score":0.2280023,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03953101584587338,"score_gpt":0.2636362021293309,"score_spread":0.2241051862834575,"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."}}