Using Hundreds of Workstations to Solve First-Order Logic Problems

Alberto Maria Segre, David B. Sturgill

This paper describes a distributed, adaptive, first-order logic engine with exceptional performance characteristics. The system combines serial search reduction techniques such as bounded-overhead subgoal caching and intelligent backtracking with a novel parallelization strategy particularly well-suited to coarse-grained parallel execution on a network of workstations. We present empirical results that demonstrate our system’s performance using 100 workstations on over 1400 first-order logic problems drawn from the "Thousands of Problems for Theorem Provers" collection.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.