{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002632056,0.0007696215,0.0006024641,0.001835541,0.001072981,0.003607846,0.001788707,0.0007081399,0.01543211],"category_scores_gemma":[0.006260542,0.00106456,0.001199487,0.001201793,0.002160953,0.004913225,0.002753617,0.003413102,0.004546367],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001572043,"about_ca_system_score_gemma":0.001212115,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0006115279,"about_ca_topic_score_gemma":0.001219258,"domain_scores_codex":[0.9980287,0.0006376202,0.00008062489,0.0002039785,0.0008978489,0.000151099],"domain_scores_gemma":[0.995749,0.003100407,0.0001548803,0.0006114494,0.0002886669,0.00009558559],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00008545872,0.00006628737,0.0004108827,0.0005932917,0.00005133275,0.0007488703,0.001086897,0.006618542,0.006455047,0.7754868,0.02596798,0.1824287],"study_design_scores_gemma":[0.00008808998,0.00007942474,0.0004392593,0.0005326826,0.0001054729,0.001299609,0.0002501286,0.04535413,0.03913119,0.5594965,0.3531374,0.00008615819],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01479623,0.003033028,0.8611687,0.001569786,0.0007378272,0.0001764938,0.0003706601,0.01151885,0.1066283],"genre_scores_gemma":[0.2650634,0.004777668,0.6570943,0.0009723246,0.0006108889,0.0002585786,0.001248592,0.008142867,0.06183135],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01543211,"threshold_uncertainty_score":0.05162561,"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."}}