Larry Wos has written many times about a technique, only one among his other techniques, for finding shorter (automated) proofs. He takes a long proof, and turns it into a large bundle of tasks, each adding to the original axioms a new axiom, something of the form "do not use step n of the long proof". Each of these proof searches can be depth-limited - you can truncate the search if the where the depth goes beyond the length of the long proof, and the "do not use" constraint can often be used productively within the search process. If there is actually a shorter proof, then at least one, and probably several, of these subtasks have a solution.
I think of this technique as "pebbling", though I am not sure whether Larry Wos would agree that this is the correct name. I think of this technique as similar to Oulipo, the french literary club where members played literary games composing works according to constraints, and more generally, lots of creativity techniques that include lists of tools or constraints such as:
- SIT's "5 thinking tools"
- De Bono's "6 thinking hats"
- IDEO's "10 faces of innovation"
- TRIZ's "40 tools"
- Brian Eno's "Oblique Strategies Deck"
- some sort of story dice?
If the direct path seems to be leading into an endless morass (for example, depth-first search without other strategies such as iterative deepening is vulnerable to getting stuck in an infinite hole) then you might put a pebble (a constraint) somewhere on the path, driving your search process off the beaten path into new territory.
If I understand the Set of Support in Otter (the tool that Larry Wos uses), it is something like a collection of potentially-generative truths or ideas; not everything that is known, but everything that is not yet exhausted. Imagine an adventure game with a binary "use X on Y" verb - if you've tried the fish with everything, then the fish is exhausted. When you get something else, like the junk mail, then you might try it in both the "use junk mail on fish" and "use fish on junk mail" orientations, but after you've used the junk mail with everything, then the junk mail is exhausted.
I believe the Knuth-Bendix procedure needs to do something similar - perhaps anytime you are systematically exploring what can be reached using a few ur-elements and a binary operation, such as resolution, condensed detachment, or "use X on Y", you might use this "Set of Support" strategy. Little Alchemy is a game that is a particularly pure example of this kind of search process.
Sometimes people configure Otter to use the Set of Support like a queue. This makes me think about a rosary, or possibly a D&D necklace of different beads, such as beads of force or summon planar ally. The necklace structure, held draped over the hand with a bead focused between finger and thumb, like a rosary, allows you to fairly easily rotate the necklace and consider potentially using (applying) each of the beads in turn, like a queue.