×

zbMATH — the first resource for mathematics

Nagging: A distributed, adversarial search-pruning technique applied to first-order inference. (English) Zbl 0884.68116
Summary: This article introduces a parallel search-pruning technique called nagging. Nagging is sufficiently general to be effective in a number of domains; here we focus on an implementation for first-order theorem proving, a domain both responsive to a very simple nagging model and amenable to many refinements of this model. Nagging’s scalability and intrinsic fault tolerance make it particularly suitable for application in commonly available, low-bandwidth, high-latency distributed environments. We present several nagging models of increasing sophistication, demonstrate their effectiveness empirically, and compare nagging with related work in parallel search.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
TPTP; SETHEO; PARTHEO
PDF BibTeX Cite
Full Text: DOI