{"id":"W2114226999","doi":"10.2178/jsl/1154698576","title":"The complexity of analytic tableaux","year":2006,"lang":"en","type":"article","venue":"Journal of Symbolic Logic","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Mathematical proof; Resolution (logic); Matching (statistics); Polynomial; Tree (set theory); Young tableau; Binary tree; Mathematics; Computer science; Combinatorics; Discrete mathematics; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.00320056,0.0004055195,0.0008351094,0.00101399,0.001541502,0.005871631,0.002046726,0.001268882,0.0120202],"category_scores_gemma":[0.0253031,0.0008008441,0.001333996,0.001200768,0.003457105,0.008313844,0.002546363,0.003227812,0.00108496],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002863363,"about_ca_system_score_gemma":0.001999564,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002230602,"about_ca_topic_score_gemma":0.001750023,"domain_scores_codex":[0.9944763,0.001925422,0.0003636432,0.0006883232,0.002061955,0.0004844764],"domain_scores_gemma":[0.9640536,0.02887459,0.001401423,0.003028327,0.002061986,0.0005801847],"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.0001378863,0.00004436698,0.0009287204,0.0002005507,0.00003479588,0.0001972476,0.0005839005,0.02541163,0.002974845,0.9497825,0.002199334,0.01750428],"study_design_scores_gemma":[0.00003924194,0.00002499523,0.0002588173,0.0000326003,0.00002642128,0.0001502965,0.0001186668,0.085485,0.004001886,0.9038203,0.006018983,0.00002289997],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2685097,0.0007333665,0.6840239,0.004709874,0.0001550172,0.0003442541,0.0009385154,0.001176007,0.03940935],"genre_scores_gemma":[0.8218466,0.0005688471,0.1650435,0.0004234154,0.0001276332,0.0002835983,0.0007680528,0.0002827403,0.01065549],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.0120202,"threshold_uncertainty_score":0.04021156,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04642661743926695,"score_gpt":0.2676815558880898,"score_spread":0.2212549384488229,"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."}}