{"id":"W1491774527","doi":"10.1007/978-3-540-70545-1_29","title":"CSIsat: Interpolation for LA+EUF","year":2008,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":62,"is_retracted":false,"has_abstract":false,"ca_institutions":"Simon Fraser University","funders":"Natural Sciences and Engineering Research Council of Canada; National Science Foundation","keywords":"Computer science; Programming language; Satisfiability modulo theories; Software; Solver; Interpolation (computer graphics); Quantifier (linguistics); Quantifier elimination; Theoretical computer science; Arithmetic; Algorithm; Mathematics; Computer graphics (images); Artificial intelligence","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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001375337,0.0004197543,0.0004092611,0.0007814358,0.0002734801,0.0003651287,0.003036172,0.000385208,0.000008303948],"category_scores_gemma":[0.0003087856,0.0004053532,0.0001582628,0.0004632004,0.0006518997,0.0009131319,0.0007327767,0.0005661192,0.00003197341],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002695313,"about_ca_system_score_gemma":0.0004306493,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000007173167,"about_ca_topic_score_gemma":0.000009929507,"domain_scores_codex":[0.9969121,0.00005637028,0.000542134,0.001283512,0.0007001813,0.0005057571],"domain_scores_gemma":[0.9971225,0.0007534555,0.000355989,0.001355452,0.0002925677,0.0001200869],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000009579374,0.00002019554,0.00001559804,0.00004015558,0.000007770276,0.00001107567,0.001166766,0.003911272,0.0001816177,0.09531643,0.0001056181,0.8992139],"study_design_scores_gemma":[0.0002294116,0.0001691485,0.0001273566,0.0002039778,0.000005456091,0.0001086161,9.454464e-8,0.8729562,0.001948572,0.1077359,0.01597777,0.0005374832],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00001585023,0.0002440347,0.9900646,0.0003104835,0.002189706,0.0005734449,0.000005479911,0.000195739,0.006400662],"genre_scores_gemma":[0.01225435,0.00006390072,0.9862687,0.0006421877,0.00039805,0.00002867212,0.000006504586,0.00003226433,0.0003053888],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8986765,"threshold_uncertainty_score":0.9998398,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03414785980137259,"score_gpt":0.2935137204647448,"score_spread":0.2593658606633722,"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."}}