Kowalski, R.


And-or graphs, theorem-proving graphs, and bi-directional search

Classics

And-or graphs and theorem-proving graphs determine the same kind of search space and differ only in the direction of search: from axioms to goals, in the case of theorem-proving graphs, and in the opposite direction, from goals to axioms, in the case of and-or graphs. We investigate the construction of a single general algorithm which covers unidirectional search both for and-or graphs and for theorem-proving graphs, bidirectional search for path-finding problems and search for a simplest solution as well as search for any solution. Indeed, many different search spaces can represent the same original problem, as in the case of resolution systems where different refinements of the resolution rule determine different search spaces for a single problem of demonstrating the unsatisfiability of a given set of clauses. In the tree representation of theorem-proving graphs (used in Machine Intelligence 5 (Kowalski 1969)), identical problems Tare generated at different times, working forwards from the initial set of axioms {D, E, F, G}.