  Temporal reasoning with conditionals is more complex than both classical
temporal reasoning and reasoning with timeless conditionals, and can lead to
some rather counter-intuitive conclusions. For instance, Aristotle's famous
"Sea Battle Tomorrow" puzzle leads to a fatalistic conclusion: whether there
will be a sea battle tomorrow or not, but that is necessarily the case now. We
propose a branching-time logic LTC to formalise reasoning about temporal
conditionals and provide that logic with adequate formal semantics. The logic
LTC extends the Nexttime fragment of CTL*, with operators for model updates,
restricting the domain to only future moments where antecedent is still
possible to satisfy. We provide formal semantics for these operators that
implements the restrictor interpretation of antecedents of temporalized
conditionals, by suitably restricting the domain of discourse. As a motivating
example, we demonstrate that a naturally formalised in our logic version of the
`Sea Battle' argument renders it unsound, thereby providing a solution to the
problem with fatalist conclusion that it entails, because its underlying
reasoning per cases argument no longer applies when these cases are treated not
as material implications but as temporal conditionals. On the technical side,
we analyze the semantics of LTC and provide a series of reductions of
LTC-formulae, first recursively eliminating the dynamic update operators and
then the path quantifiers in such formulae. Using these reductions we obtain a
sound and complete axiomatization for LTC, and reduce its decision problem to
that of the modal logic KD.
