{"id":"W2135486194","doi":"10.1109/lics.2006.19","title":"Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives","year":2006,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; National Science Foundation","keywords":"Mathematical proof; Proof complexity; Constant (computer programming); Upper and lower bounds; Sequent calculus; Mathematics; Hierarchy; Modular design; Sequent; Exponential function; Discrete mathematics; Propositional calculus; Combinatorics; Calculus (dental); Computer science; Geometry","routes":{"ca_aff":true,"ca_fund":true,"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.01055971,0.001578091,0.001530937,0.003111142,0.002713786,0.006653389,0.004742336,0.002158308,0.02144531],"category_scores_gemma":[0.06036134,0.001707792,0.003470584,0.002136216,0.005400435,0.0237325,0.01079141,0.00883249,0.002710206],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.006215684,"about_ca_system_score_gemma":0.004496158,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002286305,"about_ca_topic_score_gemma":0.002897173,"domain_scores_codex":[0.9849043,0.002562092,0.0007883077,0.003208197,0.005652148,0.002884987],"domain_scores_gemma":[0.9015588,0.07553159,0.002973158,0.01168102,0.005612919,0.002642423],"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.0007307588,0.000231193,0.002544759,0.0009297327,0.0001929576,0.0003008818,0.000903492,0.02992087,0.01621993,0.900339,0.009155342,0.03853109],"study_design_scores_gemma":[0.0001421538,0.0001370414,0.001092331,0.0001145126,0.0002425521,0.0002907762,0.00008374617,0.1628076,0.01451668,0.8100711,0.0104233,0.00007819129],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.07618698,0.001412,0.8721904,0.006784224,0.0001767128,0.0003596304,0.001162333,0.003950054,0.03777774],"genre_scores_gemma":[0.7246006,0.001365652,0.2458252,0.002510505,0.0007330027,0.0006932676,0.002504519,0.001733282,0.02003387],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.02144531,"threshold_uncertainty_score":0.0717417,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01706522866133151,"score_gpt":0.2603438644607698,"score_spread":0.2432786357994383,"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."}}