  Uniform proofs are sequent calculus proofs with the following characteristic:
the last step in the derivation of a complex formula at any stage in the proof
is always the introduction of the top-level logical symbol of that formula. We
investigate the relevance of this uniform proof notion to structuring proof
search in classical logic. A logical language in whose context provability is
equivalent to uniform provability admits of a goal-directed proof procedure
that interprets logical symbols as search directives whose meanings are given
by the corresponding inference rules. While this uniform provability property
does not hold directly of classical logic, we show that it holds of a fragment
of it that only excludes essentially positive occurrences of universal
quantifiers under a modest, sound, modification to the set of assumptions: the
addition to them of the negation of the formula being proved. We further note
that all uses of the added formula can be factored into certain derived rules.
The resulting proof system and the uniform provability property that holds of
it are used to outline a proof procedure for classical logic. An interesting
aspect of this proof procedure is that it incorporates within it previously
proposed mechanisms for dealing with disjunctive information in assumptions and
for handling hypotheticals. Our analysis sheds light on the relationship
between these mechanisms and the notion of uniform proofs.
