@Article{cmc.2026.082945,
AUTHOR = {Jordi Vallverdú},
TITLE = {A Weight-Gated Framework for Adaptive Proof Search over Fixed Base Calculi},
JOURNAL = {Computers, Materials \& Continua},
VOLUME = {},
YEAR = {},
NUMBER = {},
PAGES = {{pages}},
URL = {http://www.techscience.com/cmc/online/detail/27846},
ISSN = {1546-2226},
ABSTRACT = {Large rule-based systems—from automated theorem provers to diagnostic engines and expert systems—face a common bottleneck: when many rules are simultaneously applicable, choosing which rule to fire can dominate search effort. We present HL-W, a formally constrained adaptive proof-search control layer over a fixed base calculus. Each inference rule R is assigned a scalar weight w(R,t)∈[0,1] at search stage t; rule applications are scheduled by combining a threshold condition w(R,t)≥θ with an explicit fairness mechanism. Because the underlying inference rules are left unchanged, every derivation produced by the framework is already a derivation in the base system. Soundness and conservativity follow directly, and operational completeness is obtained relative to any complete base system under an explicit weak-fairness assumption. We also establish bounded-delay simulation under K-fair scheduling, analyse the weight dynamics via the drift threshold τ=β/(α+β), and clarify the scope of the results for monotonic and volatile-premise settings. The empirical evaluation compares HL-W with BFS, random, rule-age, static-priority, recency-based, and frequency-based conflict-resolution strategies; it also reports component-level ablation, K-sensitivity, threshold-sensitivity, parameter-sensitivity, a distractor-density stress test, and targeted adversarial controls for fairness and priority ordering. On synthetic rule graphs with |Γ|∈{5,10,20,40,60,80,100} and 300 matched trials per configuration, HL-W preserves 100% success while reducing inference steps by approximately 3× relative to BFS. Paired Wilcoxon signed-rank tests are significant in every configuration (p<0.001). A diagnostic rule-system case study similarly preserves success while reducing average inference steps from 22.43 to 14.06. Wall-clock times are reported only for transparency; the primary empirical claim is inference-step reduction under a reproducible synthetic protocol, not Python-level runtime speedup. To probe behaviour beyond the monotonic success regime, we additionally report a four-part robustness battery—an incomplete-knowledge control in which premises are randomly removed, an unsolvable-instance control, a misleading-rule control, and a conflicting-constraint control with premise retraction. The battery shows that success degrades exactly with the solvability of the base system and never with the scheduler, that HL-W never reports a derivation of a non-derivable target, and that the fairness override—dormant on the monotonic benchmark—becomes functionally necessary once a required rule schema can fall below threshold.},
DOI = {10.32604/cmc.2026.082945}
}