  Basic results in combinatorial mathematics provide the foundation for a
theory and calculus for reasoning about sequential behavior. A key concept of
the theory is a generalization of Boolean implicant which deals with statements
of the form:
  A sequence of Boolean expressions alpha is an implicant of a set of sequences
of Boolean expressions A
  This notion of a generalized implicant takes on special significance when
each of the sequences in the set A describes a disallowed pattern of behavior.
That is because a disallowed sequence of Boolean expressions represents a
logical/temporal dependency, and because the implicants of a set of disallowed
Boolean sequences A are themselves disallowed and represent precisely those
dependencies that follow as a logical consequence from the dependencies
represented by A. The main result of the theory is a necessary and sufficient
condition for a sequence of Boolean expressions to be an implicant of a regular
set of sequences of Boolean expressions. This result is the foundation for two
new proof methods. Sequential resolution is a generalization of Boolean
resolution which allows new logical/temporal dependencies to be inferred from
existing dependencies. Normalization starts with a model (system) and a set of
logical/temporal dependencies and determines which of those dependencies are
satisfied by the model.
