{"id":"W4416510022","doi":"10.1016/j.jsc.2025.102527","title":"Efficient detection of redundancies in systems of linear inequalities","year":2025,"lang":"en","type":"article","venue":"Journal of Symbolic Computation","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Western University","funders":"Mitacs; National Natural Science Foundation of China","keywords":"Redundancy (engineering); Linear inequality; Gaussian; Linear system; Software; Gaussian elimination","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.001468384,0.00006491632,0.0002660857,0.0006615845,0.00002573498,0.00001913478,0.0002540748,0.00004731333,2.545171e-7],"category_scores_gemma":[0.0002616824,0.0000602385,0.00006009245,0.0007941868,0.00004230268,0.0001578644,0.00004453434,0.0001136964,3.57197e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00009256919,"about_ca_system_score_gemma":0.0001265431,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006576915,"about_ca_topic_score_gemma":0.000002130497,"domain_scores_codex":[0.9983876,0.0002212785,0.0009335842,0.00008132084,0.0002930833,0.00008307627],"domain_scores_gemma":[0.9983103,0.0001754245,0.0008495187,0.0001291528,0.0005167995,0.00001876777],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00005751005,0.0001526057,0.0008717868,0.0004245219,0.00003031342,0.00000148794,0.00545433,0.8854925,0.03009802,0.04394251,0.00001029559,0.0334641],"study_design_scores_gemma":[0.0003895183,0.0001720749,0.02931037,0.0004060057,0.000009195471,0.00001763588,0.0006538155,0.9318258,0.03542573,0.00170402,0.00003177386,0.00005403361],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4718001,0.0002216008,0.5272709,0.00002436424,0.0005370665,0.00005854926,3.612168e-7,0.000005128723,0.00008195658],"genre_scores_gemma":[0.9348333,0.00001120506,0.06510268,0.000006411604,0.00003055247,0.000001639241,1.97125e-7,0.000002398712,0.0000116132],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.4630332,"threshold_uncertainty_score":0.2456455,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02511455571546124,"score_gpt":0.318067309482351,"score_spread":0.2929527537668898,"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."}}