Abstract
After a statement of the general problem underlying Quine's methods of simplifying logical expressions, a few examples, and a survey of various approaches to the problem, attention is focussed on the question of how to branch when the straightforward simplication rules give no further progress. An algorithm is suggested that takes advantage of the freedom of choice at the branching step in order to split the given problem into several smaller problems. As the difficulty of the problem grows exponentially with its size, this results in a great saving of effort. Both the hand and computer versions of the algorithm are described since they differ appreciably. The pattern recognition example used to illustrate the paper is chosen as typical of the wide variety of practical questions in which the above general problem arises.

This publication has 12 references indexed in Scilit: