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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX Cite
Full Text: DOI