{"id":"W2135096857","doi":"10.1007/s11787-014-0099-z","title":"Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus $${LT_\\to^{t}}$$ L T → t for Implicational Ticket Entailment","year":2014,"lang":"en","type":"article","venue":"Logica Universalis","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Alberta","funders":"","keywords":"Sequent; Sequent calculus; Natural deduction; Combinatory logic; Decidability; Mathematical proof; Mathematics; Cut-elimination theorem; Simple (philosophy); Calculus (dental); Logical consequence; Curry–Howard correspondence; Discrete mathematics; Algorithm; Computer science; Proof calculus; Programming language; Artificial intelligence; Philosophy","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.002693521,0.0005945366,0.0009222048,0.002331253,0.001611855,0.004820419,0.001876042,0.00112497,0.009719683],"category_scores_gemma":[0.01398749,0.00169382,0.002318235,0.002131522,0.001882662,0.006844409,0.004905331,0.002803425,0.003083195],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001201792,"about_ca_system_score_gemma":0.002206149,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002839256,"about_ca_topic_score_gemma":0.005399907,"domain_scores_codex":[0.9972783,0.0005356916,0.0002444302,0.000516518,0.0009621226,0.0004629437],"domain_scores_gemma":[0.9944419,0.002685733,0.0003251011,0.001445592,0.0008351258,0.0002665188],"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.0007234255,0.0002748625,0.005610342,0.0007293448,0.0001359586,0.001056846,0.002472031,0.01200429,0.02540811,0.6739388,0.007779234,0.2698668],"study_design_scores_gemma":[0.00008191182,0.00007683566,0.001378064,0.0001499048,0.0001894276,0.0003568338,0.00068746,0.07840572,0.03607256,0.862851,0.01965716,0.0000931332],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0565091,0.0002252449,0.9289407,0.0005534737,0.00009563647,0.0001677112,0.0007130709,0.004615483,0.008179496],"genre_scores_gemma":[0.3818716,0.0002763379,0.6071045,0.0001867023,0.00007494673,0.0001189973,0.00184533,0.001781469,0.006740029],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.009719683,"threshold_uncertainty_score":0.03251553,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03278948530742005,"score_gpt":0.2732889310425868,"score_spread":0.2404994457351668,"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."}}