{"id":"W4404817872","doi":"10.1007/978-981-96-0617-7_17","title":"Formalizing Potential Flows Using the HOL Light Theorem Prover","year":2024,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Numerical Methods and Algorithms","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Automated theorem proving; Computer science; Gas meter prover; Programming language; Calculus (dental); Algorithm; Theoretical computer science; Mathematics; Mathematical proof","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.002404962,0.001139974,0.0008980668,0.002045478,0.001469356,0.00464022,0.002981122,0.0009438382,0.02413626],"category_scores_gemma":[0.006229558,0.001387292,0.001833694,0.001578403,0.003121255,0.008492122,0.004423942,0.004524429,0.00629634],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001247381,"about_ca_system_score_gemma":0.001908441,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001629532,"about_ca_topic_score_gemma":0.001948172,"domain_scores_codex":[0.998234,0.0004667747,0.000137082,0.0002319469,0.0007106002,0.0002195726],"domain_scores_gemma":[0.9973852,0.001830495,0.00008483316,0.0003647987,0.0002775131,0.00005720224],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00006211567,0.00005323452,0.0001305176,0.0004092333,0.00002360362,0.00009959687,0.0002920564,0.005605965,0.002314551,0.9006888,0.0107635,0.07955676],"study_design_scores_gemma":[0.00004889686,0.00001649935,0.00005258019,0.0001361977,0.00003193298,0.0001080713,0.00008596788,0.02396235,0.009150702,0.9040481,0.06233003,0.00002868244],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002647808,0.0003405311,0.96658,0.0004517436,0.0001803572,0.0001026995,0.0004140387,0.004462767,0.02482001],"genre_scores_gemma":[0.1514457,0.001942466,0.8035498,0.0009037374,0.0003090649,0.0003966595,0.001751746,0.005407639,0.03429329],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02413626,"threshold_uncertainty_score":0.08074379,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01901458394451194,"score_gpt":0.2735598452041234,"score_spread":0.2545452612596115,"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."}}