Browse Prior Art Database

Efficient Implementation of Proboole

IP.com Disclosure Number: IPCOM000037215D
Original Publication Date: 1989-Nov-01
Included in the Prior Art Database: 2005-Jan-29
Document File: 3 page(s) / 39K

Publishing Venue

IBM

Related People

Morishita, S: AUTHOR

Abstract

Disclosed is an algorithm that enables the processor of ProBoole to run efficiently.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 53% of the total text.

Page 1 of 3

Efficient Implementation of Proboole

Disclosed is an algorithm that enables the processor of ProBoole to run efficiently.

ProBoole is a Boolean-Valued logic programming language 1, and first we introduce the implementation issue of ProBoole. The figure shows a computation of ProBoole. In a pair: SEE ORIGINAL*** is a goal, and SEE ORIGINAL* is a Boolean polynomial. When A1 and A in (SEE ORIGINAL****) are unifiable, the system derives a new pair: In this way, the system derives goals subsequently and searches Boolean polynomials which are not equivalent to 0. Thus, if is detected to be equivalent to 0, then it is useless to put forward deriving goals, and therefore the system backtracks to search for other alternative branches. This intelligent backtracking mechanism effectively reduces a search space. To do this efficiently, we require an incremental algorithm: after (SEE ORIGINAL) is proved, we should check whether or not (SEE ORIGINAL) without rechecking.

The algorithm disclosed is such an incremental algorithm which utilizes semantic resolution 2 for the propositional logic. We will use the same terminology of semantic resolution given by 3. From the completeness of semantic resolution 2, we have the following fact:(SEE ORIGINAL).

Let X be a Boolean polynomial, disjs(X) be the set of all disjunctions in a conjunctive normal form of X, and PI-deduced (disjs(X)) be the set of all disjunctions each of which has a PI-deduction from disjs(X). Then we have (SEE ORIGINAL) Then (SEE ORIGINAL) can be proved by showing: After this, in order to check whether or not , it is inefficient to construct from scratch, because the set includes PI-deduced(disjs(b1 ... bi)), which has been already obtained and checked not to contain (S...