{"id":"W2898631824","doi":"","title":"Strategy Synthesis for Linear Arithmetic Games","year":2018,"lang":"en","type":"article","venue":"Symposium on Principles of Programming Languages","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Reachability; Computer science; Satisfiability; Combinatorial game theory; Dimension (graph theory); Game theory; Game tree; Theoretical computer science; Repeated game; Sequential game; Mathematical economics; Mathematics; Combinatorics","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.001632747,0.001289324,0.0009653719,0.0009302048,0.0007949133,0.002301578,0.001239447,0.001094348,0.00783824],"category_scores_gemma":[0.006109816,0.0006435871,0.002077571,0.0006941808,0.002664755,0.002627092,0.001995671,0.002258446,0.001068146],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002417753,"about_ca_system_score_gemma":0.001953846,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002302929,"about_ca_topic_score_gemma":0.002868254,"domain_scores_codex":[0.9978306,0.0006949619,0.0001914361,0.0004589864,0.0005383633,0.0002856814],"domain_scores_gemma":[0.9978296,0.001706125,0.0001196642,0.0001274464,0.0001465867,0.0000706317],"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.0001435568,0.0001358261,0.0004068371,0.0005254467,0.00006315369,0.0001831226,0.0006336886,0.1067316,0.005970328,0.8211102,0.001693983,0.06240223],"study_design_scores_gemma":[0.0001315619,0.000119465,0.000103234,0.0001055831,0.00005724278,0.00007901206,0.0001743794,0.24038,0.005765288,0.7442479,0.00880336,0.00003291571],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02383266,0.0003880137,0.9550806,0.0005140385,0.00007516069,0.0003759517,0.0001619291,0.0008851808,0.01868643],"genre_scores_gemma":[0.3745209,0.000601756,0.6115898,0.0004250208,0.00006736191,0.0008647071,0.0005272215,0.0003163898,0.0110869],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.00783824,"threshold_uncertainty_score":0.02622157,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04412962643162666,"score_gpt":0.3367080102044734,"score_spread":0.2925783837728468,"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."}}