  Short-circuit evaluation denotes the semantics of propositional connectives
in which the second argument is evaluated only if the first argument does not
suffice to determine the value of the expression. In programming, short-circuit
evaluation is widely used, with sequential conjunction and disjunction as
primitive connectives.
  A short-circuit logic is a variant of propositional logic (PL) that can be
defined with help of Hoare's conditional, a ternary connective comparable to
if-then-else, and that implies all identities that follow from four basic
axioms for the conditional and can be expressed in PL (e.g., axioms for
associativity of conjunction and double negation shift). In the absence of side
effects, short-circuit evaluation characterizes PL. However, short-circuit
evaluation admits the possibility to model side effects and gives rise to
various different short-circuit logics. The first extreme case is FSCL (free
short-circuit logic), which characterizes the setting in which evaluation of
each atom (propositional variable) can yield a side effect. The other extreme
case is MSCL (memorizing short-circuit logic), the most identifying variant we
distinguish below PL. In MSCL, only a very restricted type of side effects can
be modelled, while sequential conjunction is non-commutative. We provide
axiomatizations for FSCL and MSCL.
  Extending MSCL with one simple axiom yields SSCL (static short-circuit logic,
or sequential PL), for which we also provide a completeness result. We briefly
discuss two variants in between FSCL and MSCL, among which a logic that admits
contraction of atoms and of their negations.
