  We present tableau calculi for some logics of nonmonotonic reasoning, as
defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for
all KLM logics, namely preferential, loop-cumulative, cumulative and rational
logics. Our calculi are obtained by introducing suitable modalities to
interpret conditional assertions. We provide a decision procedure for the
logics considered, and we study their complexity.
