{"id":"W2167987424","doi":"10.1109/time.2008.20","title":"Satisfying a Fragment of XQuery by Branching-Time Reduction","year":2008,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université du Québec à Montréal","funders":"","keywords":"Fragment (logic); Satisfiability; Computer science; XQuery; Leverage (statistics); CTL*; Branching (polymer chemistry); Boolean satisfiability problem; Decidability; Reduction (mathematics); Theoretical computer science; Algorithm; Discrete mathematics; Mathematics; Artificial intelligence; Chemistry; XML","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.0003057251,0.00006070864,0.00009197195,0.00005637914,0.00007821095,0.00001247803,0.0002835862,0.00003489831,0.00003436715],"category_scores_gemma":[0.00003747428,0.00005681821,0.00003011909,0.0002184985,0.0000418057,0.0004761242,0.00006276956,0.00005948203,0.00004089583],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003286403,"about_ca_system_score_gemma":0.00002463826,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004672252,"about_ca_topic_score_gemma":1.200222e-7,"domain_scores_codex":[0.9992448,0.00006774144,0.0002026985,0.0001772754,0.0001990604,0.0001083979],"domain_scores_gemma":[0.9994653,0.00002240423,0.00009528697,0.0003450176,0.00004004091,0.00003195185],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00001091075,0.0001432745,0.000497374,0.00003227943,0.00002102138,0.000001779552,0.002941843,0.0002703223,0.7729402,0.06220263,0.01370435,0.1472341],"study_design_scores_gemma":[0.0003250333,0.000158843,0.006377304,0.00003241803,0.000004121687,0.0001495225,0.00003136274,0.1127013,0.874534,0.002846578,0.002571432,0.0002680858],"study_design_candidate":"bench_or_experimental","study_design_consensus":"bench_or_experimental","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.1648674,0.00005929904,0.8296899,0.000118303,0.0001994128,0.00008010428,4.682545e-7,0.0001026412,0.004882475],"genre_scores_gemma":[0.3687295,0.00001784642,0.6306206,0.00003771318,0.00001807888,0.000004964881,9.017908e-7,0.000003077222,0.0005673502],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.203862,"threshold_uncertainty_score":0.2316979,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01843861241304052,"score_gpt":0.248989714332751,"score_spread":0.2305511019197105,"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."}}