{"id":"W4400169040","doi":"10.1007/978-3-031-63498-7_25","title":"A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations","year":2024,"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":"University of British Columbia","funders":"","keywords":"Computer science; Programming language; Completeness (order theory); Satisfiability modulo theories; Quantifier elimination; Matching (statistics); Theoretical computer science; Automated theorem proving; Solver; Quantifier (linguistics); Set (abstract data type); Proof assistant; Semantics (computer science); Satisfiability; Boolean satisfiability problem; Algorithm; Artificial intelligence; Mathematical proof; Mathematics","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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.0009166592,0.0003715653,0.0003338923,0.0009711877,0.0003021219,0.0009734923,0.001500062,0.0002395384,0.000001749886],"category_scores_gemma":[0.000067607,0.0003271612,0.0001367303,0.0005498676,0.0001209665,0.0008825418,0.0004588703,0.0002864145,0.00003860131],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003693211,"about_ca_system_score_gemma":0.0006825461,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001835537,"about_ca_topic_score_gemma":0.0001583917,"domain_scores_codex":[0.9971492,0.00001283312,0.0005022886,0.00109122,0.000715013,0.0005294849],"domain_scores_gemma":[0.9983912,0.0002143274,0.0002271209,0.000727036,0.0003124503,0.0001278975],"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.000003802885,0.00001834697,0.000002060465,0.0001413799,0.000006252697,0.000006114897,0.001706074,0.1767492,0.0001088106,0.5294564,0.00001828849,0.2917833],"study_design_scores_gemma":[0.0001102027,0.00012457,0.000004495638,0.00007080135,0.000006035497,0.000006727987,1.847082e-7,0.5945415,0.0003352816,0.403984,0.0005739367,0.0002422875],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.00002839774,0.00007898565,0.9932864,0.001073789,0.001570026,0.001493286,0.000009925453,0.0002772221,0.002182018],"genre_scores_gemma":[0.6371211,0.000001099609,0.3612706,0.0006812493,0.0002408706,0.0001142431,0.00001770928,0.00002822703,0.0005248518],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6370927,"threshold_uncertainty_score":0.999918,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02373044645063604,"score_gpt":0.269077801340415,"score_spread":0.245347354889779,"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."}}