Old or Heavy? Decaying Gracefully with Age/Weight Shapes.

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 congfiurable 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.

Bibliographical metadata

Original languageEnglish
Title of host publicationAutomated Deduction – CADE 27
Publication statusPublished - 20 Aug 2019
EventThe 27th International Conference on Automated Deduction - UFRN/Hotel Praiamar, Natal, Brazil
Event duration: 23 Aug 201930 Aug 2019

Publication series

NameLecture Notes in Computer Science


ConferenceThe 27th International Conference on Automated Deduction
Abbreviated titleCADE27