{"id":"W4416533042","doi":"10.1007/s10703-025-00483-4","title":"Bounded satisfiability checking of $$\\hbox {FOL}^*$$ formulas with aggregations","year":2025,"lang":"en","type":"article","venue":"Formal Methods in System Design","topic":"Advanced Software Engineering Methodologies","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"Polytechnique Montréal; University of Toronto","funders":"","keywords":"Satisfiability; Bounded function; Boolean satisfiability problem; Model checking; Constraint (computer-aided design); Automated reasoning; Satisfiability modulo theories; Constraint satisfaction problem","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.005382545,0.001171099,0.00131107,0.002071949,0.001503069,0.004214817,0.003945204,0.001255133,0.00751019],"category_scores_gemma":[0.02511502,0.001369367,0.003947265,0.001756541,0.002692709,0.006836609,0.004008772,0.002866878,0.0006787252],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003353329,"about_ca_system_score_gemma":0.005306952,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.02268356,"about_ca_topic_score_gemma":0.03448112,"domain_scores_codex":[0.9933059,0.002070297,0.0004271322,0.001161853,0.001742,0.0012929],"domain_scores_gemma":[0.9752032,0.01817251,0.001101604,0.002419787,0.002661013,0.000441841],"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.003187446,0.0009106922,0.01418807,0.001260525,0.0009671496,0.001511586,0.001185989,0.4279707,0.03391341,0.326575,0.01410073,0.1742286],"study_design_scores_gemma":[0.0001529491,0.0000783427,0.0007943498,0.0001014568,0.0002242165,0.0000866658,0.0002041042,0.8030121,0.01844119,0.1751471,0.001712523,0.00004496051],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.254918,0.0004320137,0.7263009,0.001380703,0.000218237,0.0002800306,0.001413376,0.006617618,0.008439168],"genre_scores_gemma":[0.7851562,0.0001354315,0.2081471,0.0004234427,0.00008405079,0.0001247515,0.001876659,0.0007402662,0.00331198],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.02268356,"threshold_uncertainty_score":0.04510307,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05068885233567185,"score_gpt":0.3710179682865734,"score_spread":0.3203291159509015,"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."}}