Old or Heavy? Decaying Gracefully with Age/Weight Shapes

被引:8
|
作者
Rawson, Michael [1 ]
Reger, Giles [1 ]
机构
[1] Univ Manchester, Manchester, Lancs, England
来源
AUTOMATED DEDUCTION, CADE 27 | 2019年 / 11716卷
关键词
D O I
10.1007/978-3-030-29436-6_27
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:462 / 476
页数:15
相关论文
共 50 条
  • [41] Search for the doubly heavy baryon ■ decaying to ■
    LHCb Collaboration
    [J]. Chinese Physics C., 2023, 47 (09) - 17
  • [42] LIMITS ON THE MIXING OF HEAVY DECAYING NEUTRINOS
    GRONAU, M
    [J]. PHYSICAL REVIEW D, 1983, 28 (11): : 2762 - 2766
  • [43] Looking age-appropriate while growing old gracefully: A qualitative study of ageing and body image among older adults
    Jankowski, Glen S.
    Diedrichs, Phillippa C.
    Williamson, Heidi
    Christopher, Gary
    Harcourt, Diana
    [J]. JOURNAL OF HEALTH PSYCHOLOGY, 2016, 21 (04) : 550 - 561
  • [44] Intellectual development in old age: From cross-sectional age gradients to modal shapes of change
    Lindenberger, U
    Baltes, PB
    Li, SC
    [J]. INTERNATIONAL JOURNAL OF PSYCHOLOGY, 2000, 35 (3-4) : 402 - 402
  • [45] Remodeling of heterochromatin induced by heavy metals in extreme old age
    Teimuraz Lezhava
    Jamlet Monaselidze
    Tinatin Jokhadze
    Maia Gorgoshidze
    Maia Kiladze
    Maia Gaiozishvili
    [J]. AGE, 2011, 33 : 433 - 438
  • [46] Remodeling of heterochromatin induced by heavy metals in extreme old age
    Lezhava, Teimuraz
    Monaselidze, Jamlet
    Jokhadze, Tinatin
    Gorgoshidze, Maia
    Kiladze, Maia
    Gaiozishvili, Maia
    [J]. AGE, 2011, 33 (03): : 433 - 438
  • [47] Ageing gracefully: physiology but not behaviour declines with age in a diving seabird
    Elliott, Kyle H.
    Hare, James F.
    Le Vaillant, Maryline
    Gaston, Anthony J.
    Ropert-Coudert, Yan
    Anderson, W. Gary
    [J]. FUNCTIONAL ECOLOGY, 2015, 29 (02) : 219 - 228
  • [48] Growing old gracefully? Researching OTs' attitudes to personal ageing and the elderly
    Brodala, A.
    [J]. BRITISH JOURNAL OF OCCUPATIONAL THERAPY, 2014, 77 : 85 - 86
  • [50] Body weight variability in midlife and risk for dementia in old age
    Ravona-Springer, Ramit
    Schnaider-Beeri, Michal
    Goldbourt, Uri
    [J]. NEUROLOGY, 2013, 80 (18) : 1677 - 1683