A Weight-Gated Framework for Adaptive Proof Search over Fixed Base Calculi
Jordi Vallverdú*
Philosophy Department, Universitat Autònoma de Barcelona, Bellaterra, Catalonia, Spain
* Corresponding Author: Jordi Vallverdú. Email: 
Computers, Materials & Continua https://doi.org/10.32604/cmc.2026.082945
Received 27 March 2026; Accepted 09 July 2026; Published online 06 August 2026
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.
Keywords
Adaptive inference; proof-search control; rule scheduling; weight gating; fairness; rule-based systems; automated reasoning
Open Access
Login
Register
Submit a Paper
Propose a Special lssue
Download PDF
Downloads
Citation Tools
