{"id":"W4402830973","doi":"10.21203/rs.3.rs-4974405/v1","title":"Bounded Satisfiability Checking of FOL * Formulas with Aggregations","year":2024,"lang":"en","type":"preprint","venue":"Research Square","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; National Aeronautics and Space Administration","keywords":"Bounded function; Satisfiability; Model checking; Mathematics; Discrete mathematics; Computer science; Calculus (dental); Algorithm; Mathematical analysis; Medicine","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.005915489,0.0008560814,0.001264843,0.001766805,0.001280958,0.003712179,0.002753986,0.0009069852,0.004303865],"category_scores_gemma":[0.02197612,0.00108917,0.00305168,0.002033267,0.002421884,0.006993088,0.004039173,0.002489051,0.0004920168],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002375358,"about_ca_system_score_gemma":0.002963073,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.008948867,"about_ca_topic_score_gemma":0.01197737,"domain_scores_codex":[0.9930782,0.002326392,0.0005553474,0.001102615,0.001735527,0.001201995],"domain_scores_gemma":[0.9749826,0.01762834,0.001416024,0.003719035,0.00184088,0.000413107],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.003081951,0.0007227169,0.01596015,0.000883662,0.0006171635,0.001173029,0.001303707,0.3973183,0.04503578,0.3257684,0.007023985,0.2011111],"study_design_scores_gemma":[0.00009694434,0.00006915474,0.0006583353,0.00006036151,0.0001287572,0.00006626994,0.0001408513,0.7687368,0.02100261,0.2077848,0.001224164,0.00003093989],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2291885,0.0002573668,0.7576969,0.000628666,0.00009935251,0.0001302765,0.0006014635,0.005783327,0.005614111],"genre_scores_gemma":[0.8486018,0.00007911406,0.1482384,0.0001567093,0.00006024619,0.00007707868,0.0007261902,0.0004416489,0.001618705],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.008948867,"threshold_uncertainty_score":0.03128451,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1100578308728766,"score_gpt":0.4445573786069087,"score_spread":0.3344995477340321,"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."}}