Parallel and efficient implementation of the compartmentalized connection graph proof procedure: Resolution to unification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper documents aspects of the development of a logic programming paradigm with implicit control, based in a compartmentalized con0ection graph theorem prover. Whilst the research has as it main goal the development of a language in which programs can be written with much less explicit control than PROLOG and its existing successors, a secondary goal is to exploit the immense parallelism inherent in the connection graph. This is what is in focus in this presentation. We focus initially on analysis of the extent of the parallelism inherent in the proof procedure. We characterize six different forms of parallelism These various forms of parallelism can be further classified into two classes: those associated with the performance of resolution steps, and those which are more concerned with unification. Unification is thus also a major topic of this report, and is identified as a major source of the cost of executing a logic program or proving a theorem. It turns out that deferring unification is the one of the best ways of dealing with it: hashing to perform it, and indexing to avoid it. Indexing and hashing, therefore, are our third topic.

Original languageEnglish
Title of host publicationParallelization in Inference Systems - International Workshop, Proceedings
EditorsBertram Fronhofer, Graham Wrightson
PublisherSpringer-Verlag
Pages210-233
Number of pages24
ISBN (Electronic)978-3-540-47066-3
ISBN (Print)978-3-540-55425-7
DOIs
Publication statusPublished - 1 Jan 1992
Externally publishedYes
EventInternational Workshop on Parallelization in Inference Systems, 1990 - Dagstuhl Castle, Germany
Duration: 17 Dec 199018 Dec 1990

Publication series

NameLecture Notes in Computer Science
Volume590
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Workshop on Parallelization in Inference Systems, 1990
CountryGermany
CityDagstuhl Castle
Period17/12/9018/12/90

Fingerprint Dive into the research topics of 'Parallel and efficient implementation of the compartmentalized connection graph proof procedure: Resolution to unification'. Together they form a unique fingerprint.

Cite this