  Theorem proving is one of the oldest applications which require heuristics to
prune the search space. Invertible proof procedures has been the major tool. In
this paper, we present a novel and powerful heuristic called $nongshim$ which
can be seen as an underlying principle of invertible proof procedures. Using
this heuristic, we derive an invertible sequent calculus\cite{Ketonen,Troe}
from sequent calculus for propositional logic.
