{"id":"W2012102524","doi":"10.1016/j.apal.2008.09.013","title":"On lengths of proofs in non-classical logics","year":2008,"lang":"en","type":"article","venue":"Annals of Pure and Applied Logic","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":50,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"Akademie Věd České Republiky","keywords":"Mathematical proof; Mathematics; Calculus (dental); Discrete mathematics; Algebra over a field; Pure mathematics; Geometry","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.0002739177,0.0001230112,0.0003053165,0.00008831382,0.00004256563,0.00001258187,0.0003283655,0.0001128473,0.000004052175],"category_scores_gemma":[0.0000215503,0.00008830326,0.00005272167,0.0002503621,0.0001205101,0.0000614075,0.00009811854,0.0001269432,0.0000118411],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.000003240372,"about_ca_system_score_gemma":0.00002719957,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000009206922,"about_ca_topic_score_gemma":0.0000067725,"domain_scores_codex":[0.9989923,0.00002681367,0.0002784718,0.0002724344,0.0002047428,0.0002252774],"domain_scores_gemma":[0.999413,0.00007987925,0.0001395167,0.0002629575,0.00004773925,0.00005693193],"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.00002143372,0.0002800606,0.0006641306,0.00005739131,0.00001050377,0.00002179182,0.0006602566,0.0000484613,0.0006343769,0.9760092,0.001345893,0.02024649],"study_design_scores_gemma":[0.001716283,0.002395117,0.0246624,0.00004091529,0.000009992124,0.00005833666,0.0002260046,0.001795496,0.03650777,0.923324,0.008560605,0.000703063],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7658982,0.00137925,0.09467657,0.002744077,0.000327744,0.001400722,0.000003699313,0.0001535546,0.1334162],"genre_scores_gemma":[0.9986053,0.00009144114,0.0007646056,0.0003690761,0.00003518426,0.00001656434,0.000001338935,0.000004077012,0.0001124244],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.2327071,"threshold_uncertainty_score":0.3600902,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05842729758352427,"score_gpt":0.282818869212485,"score_spread":0.2243915716289607,"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."}}