zbMATH — the first resource for mathematics

Old or heavy? Decaying gracefully with age/weight shapes. (English) Zbl 07178992
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 462-476 (2019).
Summary: Modern saturation theorem provers are based on the given-clause algorithm, which iteratively selects new clauses to process. This clause selection has a large impact on the performance of proof search and has been the subject of much folklore. The standard approach is to alternate between selecting the oldest clause and the lightest clause with a fixed, but configurable age/weight ratio (AWR). An optimal fixed value of this ratio is shown to produce proofs significantly more quickly on a given problem, and further that varying AWR during proof search can improve upon a fixed ratio. Several new modes for the Vampire prover which vary AWR according to a “shape” during proof search are developed based on these observations. The modes solve a number of new problems in the TPTP benchmark set.
For the entire collection see [Zbl 1428.68018].

03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI