The DALI theorem prover is a distributed inference engine for first order logic. The design is based on an extended version of the Warren Abstract Machine architecture. Some of these extensions, inspired by Mark Stickel's work on the PTTP system, circumvent the inherent limitations of Prolog to provide first-order completeness. These extensions include support for sound unification, iterative deepening, and model elimination.

A second set of extensions, based in part on our own previous work in speedup learning techniques for theorem proving, serves to improve efficiency and performance. These extensions provide support for bounded-overhead subgoal caching, explanation-based learning, and intelligent backtracking.

The final set of extensions supports a novel asynchronous parallelism scheme called nagging. Nagging is particularly appropriate for highly-constrained nondeterministic search problems characterized by very large search spaces. Its advantages include low communication costs, natural fault tolerance, and excellent scalability. A prototype implementation of this inference engine design uses a loosely-coupled heterogeneous network of workstations to solve large search problems.