  A sound and complete embedding of conditional logics into classical
higher-order logic is presented. This embedding enables the application of
off-the-shelf higher-order automated theorem provers and model finders for
reasoning within and about conditional logics.
