Partial instantiation theorem proving for distributed resource location

Author

Vanderveen, Keith ; Ramamoorthy, C.V.

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA

fYear

1997

fDate

11-15 Aug 1997

Firstpage

192

Lastpage

197

Abstract

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

Keywords

computability; distributed processing; formal logic; object-oriented methods; parallel algorithms; resource allocation; theorem proving; CORBA Object Trading Service; GSAT algorithm; INSTANT; KIF; KQML; clausal form; distributed resource location; first order logic; non clausal form; partial instantiation theorem prover; propositional sentence; request matching; satisfiability; Application software; Artificial intelligence; Availability; Hardware; Information systems; Logic; Resource management; Software agents; System software; Terminology;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1997. COMPSAC '97. Proceedings., The Twenty-First Annual International

Conference_Location

Washington, DC

ISSN

0730-3157

Print_ISBN

0-8186-8105-5

Type

conf

DOI

10.1109/CMPSAC.1997.624790

Filename

624790