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.

翻译：时间条件句推理比经典时间推理和无时间条件句推理更为复杂，且可能导致某些相当反直觉的结论。例如，亚里士多德著名的"明日海战"谜题会推导出宿命论结论：无论明日是否会发生海战，该结果现在都必然成立。我们提出分支时间逻辑LTC以形式化时间条件句推理，并为该逻辑提供充分的形式语义。LTC逻辑扩展了CTL*的Nexttime片段，引入了模型更新算子，将论域限制在前提仍可能满足的未来时刻。我们通过适当限制论域，为这些算子提供形式语义，从而实现对时间化条件句前件的限制器解释。作为示例，我们证明：在本逻辑中自然形式化的"海战"论证版本会使其丧失可靠性，由此为该论证所蕴含的宿命论结论问题提供解决方案——当这些情形不再被视为实质蕴涵而是作为时间条件句处理时，其基于分情形论证的底层推理便不再适用。在技术层面，我们分析LTC的语义，并给出LTC公式的系列归约方法：先递归消除动态更新算子，再消除公式中的路径量词。通过这些归约，我们获得了LTC的可靠且完备的公理化系统，并将其判定问题归约为模态逻辑KD的判定问题。