{"id":"W4412898049","doi":"10.1007/978-3-031-99984-0_30","title":"Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL","year":2025,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"","keywords":"HOL; Mathematical proof; Computer science; Programming language; Automated theorem proving; Mathematics","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.0007626356,0.00042228,0.0004974708,0.0009033637,0.000255897,0.0006520665,0.002134051,0.0003467261,0.00001113394],"category_scores_gemma":[0.000148933,0.0003981112,0.0001037554,0.0009908456,0.000246118,0.000755223,0.0009161624,0.0006745486,0.00003451256],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003492533,"about_ca_system_score_gemma":0.0005518897,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002404454,"about_ca_topic_score_gemma":0.0006048221,"domain_scores_codex":[0.9964866,0.00006181744,0.0006895532,0.001457946,0.0007345337,0.0005695556],"domain_scores_gemma":[0.9978039,0.0004684174,0.0003358377,0.001113818,0.0001838726,0.00009414071],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000002878058,0.0000458929,0.001355552,0.0000441863,0.00001138174,0.00004195182,0.00188215,0.01299098,0.00006524476,0.2219701,0.00002019982,0.7615695],"study_design_scores_gemma":[0.0003432029,0.00006475207,0.0005940496,0.000253644,0.000006104724,0.000007415743,7.827437e-7,0.5021088,0.0005132716,0.4928764,0.002676827,0.0005547597],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0001885583,0.0005352104,0.9880946,0.0004300172,0.001859611,0.0006529164,0.000002993987,0.0001903706,0.008045723],"genre_scores_gemma":[0.8743727,0.00002183851,0.124134,0.0005107935,0.000367529,0.00003235217,0.00001981878,0.00001991156,0.0005210959],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8741841,"threshold_uncertainty_score":0.9998471,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0265450523097481,"score_gpt":0.2527169389653506,"score_spread":0.2261718866556025,"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."}}