Partial instantiation theorem proving for distributed resource location

We present a partial instantiation theorem prover (INSTANT) which handles sentences in first order logic in clausal or non clausal form. INSTANT uses a variant of the GSAT algorithm for determining the satisfiability of a propositional sentence to increase its speed. The algorithm used in INSTANT can be parallelized with good speedup to improve performance. INSTANT is designed for matching requests for resources with available resources over a network. Environments in which distributed resource location takes place through matching of requests and advertisements include CORBA´s Object Trading Service and communication between agents using KIF and KQML