{"id":"W4206670752","doi":"10.1145/3498722","title":"Solving constrained Horn clauses modulo algebraic data types and recursive functions","year":2022,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":26,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"European Research Council; European Commission; Natural Sciences and Engineering Research Council of Canada; United States-Israel Binational Science Foundation; Israel Science Foundation; United States - Israel Binational Science Foundation","keywords":"Decidability; Correctness; Modulo; Computer science; RDF Schema; Theoretical computer science; Undecidable problem; Counterexample; Programming language; Discrete mathematics; Mathematics; RDF; 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":[],"consensus_categories":[],"category_scores_codex":[0.0008496116,0.0001187518,0.0001341833,0.0001009652,0.0004205044,0.000146259,0.003395239,0.00003182387,0.000008577587],"category_scores_gemma":[0.002012697,0.00009450028,0.00003459334,0.0004917491,0.0001479683,0.0004804425,0.003541284,0.0002501993,0.000001663523],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003415877,"about_ca_system_score_gemma":0.00003128259,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002375338,"about_ca_topic_score_gemma":0.00000147159,"domain_scores_codex":[0.9988374,0.00002966145,0.0001897985,0.0004077206,0.0003227608,0.0002126382],"domain_scores_gemma":[0.9986148,0.0001224492,0.0002524653,0.0008674148,0.0001024692,0.00004039472],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00005870684,0.0002423113,0.003373227,0.0001966001,0.0001331118,0.000001951086,0.007760612,0.00003106561,0.01533467,0.2552584,0.005550955,0.7120584],"study_design_scores_gemma":[0.005484041,0.007217984,0.0383205,0.001431537,0.0009964785,0.00157217,0.1352766,0.07096664,0.2547732,0.254214,0.224705,0.005041797],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9759399,0.002336842,0.007966795,0.007696605,0.001042124,0.001513766,0.00007422585,0.0008005776,0.002629195],"genre_scores_gemma":[0.5868927,0.00001433949,0.4126042,0.0001850541,0.0000474197,0.00006838985,0.000006131187,0.0000133915,0.0001684207],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.7070166,"threshold_uncertainty_score":0.6309254,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03735519205231355,"score_gpt":0.2969661613641396,"score_spread":0.259610969311826,"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."}}