  The proof search approach views the state of a computation as a sequent (a structured collection of formulas) and the process of computing as the process of searching for a proof of a sequent: the changes that take place in sequents capture the dynamics of computation.  With this view of computation, we generally read inference rules bottom up, i.e.,  as a transformation of their conclusion into their premise(s).  Logic programming can be explained using proof search as its theoretical basis, and linear logic provides this approach to computational specification with new combinators for building logic programs, new means to capture rich dynamics, and new declarative approaches to specifying concurrent computations. (See  Miller 2004  for an overview of linear logic programming languages.)