{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002220401,0.0009166442,0.0006267638,0.0009597327,0.0007609124,0.001670403,0.001766297,0.001023819,0.004375063],"category_scores_gemma":[0.007598279,0.0006434608,0.002358764,0.000937973,0.001870045,0.003808451,0.002319683,0.002275627,0.0006052522],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001615059,"about_ca_system_score_gemma":0.002944146,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006001977,"about_ca_topic_score_gemma":0.009994038,"domain_scores_codex":[0.997927,0.0004852797,0.0001646304,0.0005737877,0.0005203998,0.0003289647],"domain_scores_gemma":[0.9938996,0.004574563,0.0004313968,0.0005629277,0.0004421973,0.00008929373],"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.0004438191,0.0003662959,0.004805855,0.001479904,0.0002458524,0.0008777948,0.0009797133,0.2348375,0.02615946,0.4409695,0.00813388,0.2807006],"study_design_scores_gemma":[0.000152383,0.0001331865,0.000439905,0.0001088484,0.0001274435,0.0002905323,0.0002738764,0.595071,0.03610642,0.3582685,0.008976737,0.00005116493],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0569926,0.0002542215,0.9341004,0.000840291,0.00007006102,0.0002275491,0.0004271326,0.002636721,0.004451028],"genre_scores_gemma":[0.2789185,0.0002449762,0.7153522,0.0004988638,0.00007891184,0.0001582292,0.001268124,0.0005040328,0.002976163],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006001977,"threshold_uncertainty_score":0.01463604,"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."}}