diff --git a/src/app.py b/src/app.py
index b61d328..74dcff4 100644
--- a/src/app.py
+++ b/src/app.py
@@ -322,7 +322,7 @@ def ltl_to_english():
         return jsonify({"error": "Missing required query parameter 'formula'."}), 400
     try:
         node = parse_ltl_string(formula)
-        english = ltltoeng.finalize_sentence(node.__to_english__())
+        english = ltltoeng.translate(node, discourse=True)
     except Exception as e:
         return jsonify({"error": "Failed to translate formula.", "details": str(e)}), 400
 
@@ -426,7 +426,7 @@ def ltl_to_english_ui():
         else:
             try:
                 node = parse_ltl_string(input_formula)
-                translation = ltltoeng.finalize_sentence(node.__to_english__())
+                translation = ltltoeng.translate(node, discourse=True)
             except Exception as e:
                 error = f"Failed to translate formula: {e}"
 
diff --git a/src/exercisebuilder.py b/src/exercisebuilder.py
index 3e769d9..7152691 100644
--- a/src/exercisebuilder.py
+++ b/src/exercisebuilder.py
@@ -54,7 +54,7 @@ def getLTLFormulaAsString(self, node):
         elif self.syntax == "English":
             ## We should hopefully never get here. However, 
             ## I'm adding it here to suggest a way forward.
-            return node.__to_english__()
+            return ltltoeng.translate(node, discourse=True)
 
         ## Default to classic syntax
         return str(node)
@@ -492,14 +492,14 @@ def formula_choice_metric(formula):
     def gen_nl_question(self, formula):
 
         as_node = ltlnode.parse_ltl_string(formula)
-        formula_eng = as_node.__to_english__()
+        formula_eng = ltltoeng.translate(as_node, discourse=True)
         if formula_eng is None or formula_eng == "":
             return None
         
         formula_eng_corrected = ltltoeng.correct_grammar(formula_eng)
         ### If there are multiple '.' in a row, replace with a single '.'
         formula_eng_corrected = re.sub(r'\.{2,}', '.', formula_eng_corrected)
-        return ltltoeng.finalize_sentence(formula_eng_corrected)
+        return formula_eng_corrected
 
 
     def get_options_with_misconceptions_as_formula(self, answer):
diff --git a/src/ltlir.py b/src/ltlir.py
new file mode 100644
index 0000000..4cd285f
--- /dev/null
+++ b/src/ltlir.py
@@ -0,0 +1,25 @@
+from dataclasses import dataclass, field
+from typing import List, Optional
+
+
+@dataclass
+class PlanStep:
+    """Intermediate representation step for discourse planning."""
+    role: str  # "anchor", "lead", "clause"
+    text: str
+    prefix: Optional[str] = None
+
+
+@dataclass
+class TemporalPlan:
+    """Intermediate compiled plan for multi-sentence LTL translations."""
+    steps: List[PlanStep] = field(default_factory=list)
+
+    def add_anchor(self, text: str) -> None:
+        self.steps.append(PlanStep(role="anchor", text=text))
+
+    def add_lead(self, text: str) -> None:
+        self.steps.append(PlanStep(role="lead", text=text))
+
+    def add_clause(self, text: str, prefix: Optional[str] = None) -> None:
+        self.steps.append(PlanStep(role="clause", text=text, prefix=prefix))
diff --git a/src/ltlnode.py b/src/ltlnode.py
index 117f057..eaf6d53 100644
--- a/src/ltlnode.py
+++ b/src/ltlnode.py
@@ -308,22 +308,17 @@ class FinallyNode(UnaryOperatorNode):
     def __init__(self, operand):
         super().__init__(FinallyNode.symbol, operand)
 
-    def __to_english__(self):
-        x = ltltoeng.apply_special_pattern_if_possible(self)
-        if x is not None:
-            return x
-        op = self.operand.__to_english__().rstrip('.')
-
-        # Provide more natural alternatives
-        if type(self.operand) is LiteralNode:
-            patterns = [
-                f"eventually, {op}",
-                f"{op} will eventually occur",
-                f"at some point, {op} will hold"
-            ]
-            return ltltoeng.choose_best_sentence(patterns)
-        
-        return f"eventually, {op}"
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        op = self.operand.__to_english__().rstrip('.')
+
+        # Provide more natural alternatives
+        if type(self.operand) is LiteralNode:
+            return ltltoeng.finally_phrase(op, is_literal=True)
+
+        return ltltoeng.finally_phrase(op, is_literal=False)
     
     def __forge__(self):
         return f"(EVENTUALLY {self.operand.__forge__()})"
@@ -339,23 +334,20 @@ class OrNode(BinaryOperatorNode):
     def __init__(self, left, right):
         super().__init__(OrNode.symbol, left, right)
 
-    def __to_english__(self):
-        x = ltltoeng.apply_special_pattern_if_possible(self)
-        if x is not None:
-            return x
-        lhs = self.left.__to_english__().rstrip('.')
-        rhs = self.right.__to_english__().rstrip('.')
-        
-        # Provide alternatives for simple literals
-        if type(self.left) is LiteralNode and type(self.right) is LiteralNode:
-            patterns = [
-                f"either {lhs} or {rhs}",
-                f"{lhs} or {rhs}",
-                f"at least one of {lhs} or {rhs}"
-            ]
-            return ltltoeng.choose_best_sentence(patterns)
-        
-        return f"either {lhs} or {rhs}"
+    def __to_english__(self):
+        x = ltltoeng.apply_special_pattern_if_possible(self)
+        if x is not None:
+            return x
+        lhs = self.left.__to_english__().rstrip('.')
+        rhs = self.right.__to_english__().rstrip('.')
+        
+        # Provide alternatives for simple literals
+        if type(self.left) is LiteralNode and type(self.right) is LiteralNode:
+            return ltltoeng.or_phrase(lhs, rhs)
+
+        if ltltoeng.get_pragmatic_policy().avoid_exclusive_or:
+            return f"either {lhs} or {rhs} (or both)"
+        return f"either {lhs} or {rhs}"
     
 
 
@@ -365,7 +357,7 @@ class AndNode(BinaryOperatorNode):
     def __init__(self, left, right):
         super().__init__(AndNode.symbol, left, right)
 
-    def __to_english__(self):
+    def __to_english__(self):
         x = ltltoeng.apply_special_pattern_if_possible(self)
         if x is not None:
             return x
@@ -423,16 +415,17 @@ def __to_english__(self):
         lhs = ltltoeng.normalize_embedded_clause(lhs)
         rhs = ltltoeng.normalize_embedded_clause(rhs)
 
-        # Potential patterns:
-        patterns = [
-            f"if {lhs}, then {rhs}",
-            f"{lhs} implies {rhs}",
-            f"whenever {lhs}, then {rhs}"
-        ]
-
-        # Choose the most fluent pattern rather than picking randomly
-        english = ltltoeng.choose_best_sentence(patterns)
-        return english
+        # Potential patterns:
+        patterns = [
+            f"if {lhs}, then {rhs}",
+            f"{lhs} implies {rhs}"
+        ]
+        if not ltltoeng.get_pragmatic_policy().avoid_causal:
+            patterns.append(f"whenever {lhs}, {rhs}")
+
+        # Choose the most fluent pattern rather than picking randomly
+        english = ltltoeng.choose_best_sentence(patterns)
+        return english
 
 
 class EquivalenceNode(BinaryOperatorNode):
diff --git a/src/ltltoeng.py b/src/ltltoeng.py
index cb71e9c..60c52c0 100644
--- a/src/ltltoeng.py
+++ b/src/ltltoeng.py
@@ -1,11 +1,43 @@
-import ltlnode
-import random
-import re
+import ltlnode
+import ltlir
+import random
+import re
+from dataclasses import dataclass
+from contextlib import contextmanager
 
 import inflect
 from wordfreq import zipf_frequency
 
-_inflect_engine = inflect.engine()
+_inflect_engine = inflect.engine()
+
+
+@dataclass
+class PragmaticPolicy:
+    """Controls pragmatic inferences in LTL->English rendering."""
+    avoid_exclusive_or: bool = True
+    allow_now_in_eventually: bool = True
+    avoid_deontic: bool = True
+    avoid_causal: bool = True
+    explicit_weak_until: bool = True
+
+
+_PRAGMATIC_POLICY = PragmaticPolicy()
+
+
+def get_pragmatic_policy():
+    return _PRAGMATIC_POLICY
+
+
+@contextmanager
+def _use_pragmatic_policy(policy):
+    global _PRAGMATIC_POLICY
+    prev = _PRAGMATIC_POLICY
+    if policy is not None:
+        _PRAGMATIC_POLICY = policy
+    try:
+        yield
+    finally:
+        _PRAGMATIC_POLICY = prev
 
 ## We should list the various patterns of LTL formulae that we can handle
 
@@ -186,12 +218,161 @@ def normalize_embedded_clause(text):
     return t
 
 
-def finalize_sentence(text):
-    """Apply smoothing and capitalization once, at the top level."""
-    if text is None:
-        return ""
-    smoothed = smooth_grammar(text.strip())
-    return capitalize_sentence(smoothed)
+def finalize_sentence(text):
+    """Apply smoothing and capitalization once, at the top level."""
+    if text is None:
+        return ""
+    smoothed = smooth_grammar(text.strip())
+    return capitalize_sentence(smoothed)
+
+
+def _conditional_word():
+    return "if" if get_pragmatic_policy().avoid_causal else "whenever"
+
+
+def _deontic_variants(neutral_variants, deontic_variants):
+    if get_pragmatic_policy().avoid_deontic:
+        return neutral_variants
+    return neutral_variants + deontic_variants
+
+
+def or_phrase(lhs, rhs):
+    policy = get_pragmatic_policy()
+    if policy.avoid_exclusive_or:
+        patterns = [
+            f"one or both of {lhs} and {rhs}",
+            f"{lhs} or {rhs} (or both)",
+            f"at least one of {lhs} or {rhs} (possibly both)"
+        ]
+    else:
+        patterns = [
+            f"either {lhs} or {rhs}",
+            f"{lhs} or {rhs}",
+            f"at least one of {lhs} or {rhs}"
+        ]
+    return choose_best_sentence(patterns)
+
+
+def finally_phrase(op, is_literal=False):
+    patterns = []
+    if get_pragmatic_policy().allow_now_in_eventually:
+        patterns.append(f"now or later, {op}")
+        patterns.append(f"at some point, possibly now, {op}")
+    if is_literal:
+        patterns.extend([
+            f"eventually, {op}",
+            f"{op} will eventually occur",
+            f"at some point, {op} will hold"
+        ])
+    else:
+        patterns.append(f"eventually, {op}")
+    return choose_best_sentence(patterns)
+
+
+def _embedded_clause(node):
+    """Return a clause suitable for embedding after a discourse prefix."""
+    text = clean_for_composition(node.__to_english__())
+    return normalize_embedded_clause(text)
+
+
+def _node_size(node):
+    if isinstance(node, ltlnode.UnaryOperatorNode):
+        return 1 + _node_size(node.operand)
+    if isinstance(node, ltlnode.BinaryOperatorNode):
+        return 1 + _node_size(node.left) + _node_size(node.right)
+    return 1
+
+
+def _temporal_op_count(node):
+    count = 0
+    if isinstance(node, (ltlnode.NextNode, ltlnode.FinallyNode, ltlnode.GloballyNode, ltlnode.UntilNode)):
+        count += 1
+    if isinstance(node, ltlnode.UnaryOperatorNode):
+        return count + _temporal_op_count(node.operand)
+    if isinstance(node, ltlnode.BinaryOperatorNode):
+        return count + _temporal_op_count(node.left) + _temporal_op_count(node.right)
+    return count
+
+
+def _should_split_conjunction(node):
+    if not isinstance(node, (ltlnode.AndNode, ltlnode.OrNode)):
+        return False
+    left_ops = _temporal_op_count(node.left)
+    right_ops = _temporal_op_count(node.right)
+    total_ops = left_ops + right_ops
+    total_size = _node_size(node)
+    return total_ops >= 2 or total_size >= 8
+
+
+def _eventual_anchor_phrasing():
+    return (
+        choose_best_sentence([
+            "eventually we reach a point in time",
+            "eventually there is a point in time",
+            "eventually a point is reached"
+        ]),
+        "from then on"
+    )
+
+
+def build_discourse_plan(node):
+    """Compile select LTL forms into a discourse-oriented plan."""
+    # Eventual permanence: F(G φ) -> anchor + "from then on" clause
+    if isinstance(node, ltlnode.FinallyNode) and isinstance(node.operand, ltlnode.GloballyNode):
+        anchor_sentence, prefix = _eventual_anchor_phrasing()
+        inner = node.operand.operand
+        plan = ltlir.TemporalPlan()
+        plan.add_anchor(anchor_sentence)
+        plan.add_clause(_embedded_clause(inner), prefix=prefix)
+        return plan
+
+    # Split large conjunctions into two sentences
+    if isinstance(node, ltlnode.AndNode) and _should_split_conjunction(node):
+        plan = ltlir.TemporalPlan()
+        lead = "both of the following hold" if get_pragmatic_policy().avoid_deontic else "both of the following must hold"
+        plan.add_lead(lead)
+        plan.add_clause(_embedded_clause(node.left), prefix="first")
+        plan.add_clause(_embedded_clause(node.right), prefix="second")
+        return plan
+
+    # Split large disjunctions into two sentences
+    if isinstance(node, ltlnode.OrNode) and _should_split_conjunction(node):
+        plan = ltlir.TemporalPlan()
+        lead = "at least one of the following holds" if get_pragmatic_policy().avoid_deontic else "at least one of the following must hold"
+        plan.add_lead(lead)
+        left_clause = _embedded_clause(node.left)
+        right_clause = _embedded_clause(node.right)
+        plan.add_clause(f"either {left_clause} or {right_clause}")
+        return plan
+
+    return None
+
+
+def render_discourse_plan(plan):
+    sentences = []
+    for step in plan.steps:
+        text = step.text
+        if step.prefix:
+            text = f"{step.prefix}, {text}"
+        sentence = finalize_sentence(text)
+        if sentence:
+            sentences.append(sentence)
+    return ". ".join(sentences)
+
+
+def to_english_discourse(node):
+    plan = build_discourse_plan(node)
+    if plan:
+        return render_discourse_plan(plan)
+    return finalize_sentence(node.__to_english__())
+
+
+def translate(node, discourse=False, policy=None):
+    """Top-level translation entrypoint with optional discourse planning and pragmatics."""
+    with _use_pragmatic_policy(policy):
+        if discourse:
+            return to_english_discourse(node)
+        return finalize_sentence(node.__to_english__())
 
 
 def _ngram_fluency_score(text):
@@ -299,55 +480,67 @@ def until_in_or_precedence_pattern(node):
 # English: p holds at all times / p always holds
 # More natural phrasings for simple globally of a literal
 @pattern
-def globally_literal_pattern_to_english(node):
+def globally_literal_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.LiteralNode:
-            lit_eng = clean_for_composition(op.__to_english__())
-            patterns = [
-                f"{lit_eng} holds at all times",
-                f"{lit_eng} always holds",
-                f"{lit_eng} must always hold",
-                f"at all times, {lit_eng} holds"
-            ]
-            return choose_best_sentence(patterns)
-    return None
+            lit_eng = clean_for_composition(op.__to_english__())
+            patterns = _deontic_variants(
+                [
+                    f"{lit_eng} holds at all times",
+                    f"{lit_eng} always holds",
+                    f"at all times, {lit_eng} holds"
+                ],
+                [
+                    f"{lit_eng} must always hold"
+                ]
+            )
+            return choose_best_sentence(patterns)
+    return None
 
 
 # G (p & q) - globally conjunction
 # English: always maintain both p and q / both p and q hold at all times
 @pattern
-def globally_and_pattern_to_english(node):
+def globally_and_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.AndNode:
-            left_eng = clean_for_composition(op.left.__to_english__())
-            right_eng = clean_for_composition(op.right.__to_english__())
-            patterns = [
-                f"always maintain both {left_eng} and {right_eng}",
-                f"both {left_eng} and {right_eng} must always hold",
-                f"at all times, both {left_eng} and {right_eng} hold"
-            ]
-            return choose_best_sentence(patterns)
-    return None
+            left_eng = clean_for_composition(op.left.__to_english__())
+            right_eng = clean_for_composition(op.right.__to_english__())
+            patterns = _deontic_variants(
+                [
+                    f"always maintain both {left_eng} and {right_eng}",
+                    f"at all times, both {left_eng} and {right_eng} hold"
+                ],
+                [
+                    f"both {left_eng} and {right_eng} must always hold"
+                ]
+            )
+            return choose_best_sentence(patterns)
+    return None
 
 
 # G (p | q) - globally disjunction
 # English: always have either p or q / either p or q holds at all times
 @pattern
-def globally_or_pattern_to_english(node):
+def globally_or_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.OrNode:
-            left_eng = clean_for_composition(op.left.__to_english__())
-            right_eng = clean_for_composition(op.right.__to_english__())
-            patterns = [
-                f"always have either {left_eng} or {right_eng}",
-                f"either {left_eng} or {right_eng} must always hold",
-                f"at all times, either {left_eng} or {right_eng} holds"
-            ]
-            return choose_best_sentence(patterns)
-    return None
+            left_eng = clean_for_composition(op.left.__to_english__())
+            right_eng = clean_for_composition(op.right.__to_english__())
+            patterns = _deontic_variants(
+                [
+                    f"always have either {left_eng} or {right_eng}",
+                    f"at all times, either {left_eng} or {right_eng} holds"
+                ],
+                [
+                    f"either {left_eng} or {right_eng} must always hold"
+                ]
+            )
+            return choose_best_sentence(patterns)
+    return None
 
 
 # G G ... G p (idempotent globally - G G = G)
@@ -372,7 +565,7 @@ def idempotent_globally_pattern_to_english(node):
 # Note: We check that left is not an UntilNode to allow more specific patterns to match first
 
 @pattern
-def response_pattern_to_english(node):
+def response_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.ImpliesNode:
@@ -381,10 +574,12 @@ def response_pattern_to_english(node):
             # Skip if left is Until - let more specific pattern handle it
             if type(left) is ltlnode.UntilNode:
                 return None
-            if type(right) is ltlnode.FinallyNode:
-                left_eng = clean_for_composition(left.__to_english__())
-                right_eng = clean_for_composition(right.operand.__to_english__())
-                return f"whenever {left_eng}, eventually {right_eng}"
+            if type(right) is ltlnode.FinallyNode:
+                left_eng = clean_for_composition(left.__to_english__())
+                right_eng = clean_for_composition(right.operand.__to_english__())
+                if get_pragmatic_policy().avoid_causal:
+                    return f"if {left_eng}, then eventually {right_eng}"
+                return f"whenever {left_eng}, eventually {right_eng}"
             
     return None
 
@@ -486,7 +681,7 @@ def final_state_globally_pattern(node):
 # English: Whenever p (happens), q will (hold) until r (holds)
 
 @pattern
-def chain_precedence_pattern_to_english(node):
+def chain_precedence_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.ImpliesNode:
@@ -495,18 +690,20 @@ def chain_precedence_pattern_to_english(node):
             if type(right) is ltlnode.UntilNode:
                 lhs = right.left
                 rhs = right.right
-                left_eng = clean_for_composition(left.__to_english__())
-                lhs_eng = clean_for_composition(lhs.__to_english__())
-                rhs_eng = clean_for_composition(rhs.__to_english__())
-                return f"whenever {left_eng}, {lhs_eng} until {rhs_eng}"
-    return None
+                left_eng = clean_for_composition(left.__to_english__())
+                lhs_eng = clean_for_composition(lhs.__to_english__())
+                rhs_eng = clean_for_composition(rhs.__to_english__())
+                if get_pragmatic_policy().avoid_causal:
+                    return f"if {left_eng}, then {lhs_eng} until {rhs_eng}"
+                return f"whenever {left_eng}, {lhs_eng} until {rhs_eng}"
+    return None
 
 
 ## Chain response
 # Pattern: G (p -> ( (F q) & (F r) ) )
 # English: Whenever p (holds), q and r will (hold) eventually
 @pattern
-def chain_response_pattern_to_english(node):
+def chain_response_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.ImpliesNode:
@@ -515,12 +712,14 @@ def chain_response_pattern_to_english(node):
             if type(right) is ltlnode.AndNode:
                 lhs = right.left
                 rhs = right.right
-                if type(lhs) is ltlnode.FinallyNode and type(rhs) is ltlnode.FinallyNode:
-                    left_eng = clean_for_composition(left.__to_english__())
-                    lhs_eng = clean_for_composition(lhs.operand.__to_english__())
-                    rhs_eng = clean_for_composition(rhs.operand.__to_english__())
-                    return f"whenever {left_eng}, eventually {lhs_eng} and {rhs_eng}"
-    return None
+                if type(lhs) is ltlnode.FinallyNode and type(rhs) is ltlnode.FinallyNode:
+                    left_eng = clean_for_composition(left.__to_english__())
+                    lhs_eng = clean_for_composition(lhs.operand.__to_english__())
+                    rhs_eng = clean_for_composition(rhs.operand.__to_english__())
+                    if get_pragmatic_policy().avoid_causal:
+                        return f"if {left_eng}, then eventually {lhs_eng} and {rhs_eng}"
+                    return f"whenever {left_eng}, eventually {lhs_eng} and {rhs_eng}"
+    return None
 
 
 ## Immediate Response Pattern
@@ -529,7 +728,7 @@ def chain_response_pattern_to_english(node):
 # Source: Dwyer, M.B., Avrunin, G.S., Corbett, J.C. "Patterns in Property Specifications for Finite-State Verification"
 #         Proceedings of ICSE 1999. http://patterns.projects.cs.ksu.edu/
 @pattern
-def immediate_response_pattern_to_english(node):
+def immediate_response_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.ImpliesNode:
@@ -537,14 +736,17 @@ def immediate_response_pattern_to_english(node):
             right = op.right
             if type(right) is ltlnode.NextNode:
                 # Don't match if it's the final state pattern G(p -> X p)
-                if (type(left) is ltlnode.LiteralNode and 
-                    type(right.operand) is ltlnode.LiteralNode and
-                    left.value == right.operand.value):
-                    return None
-                left_eng = clean_for_composition(left.__to_english__())
-                right_eng = clean_for_composition(right.operand.__to_english__())
-                return f"whenever {left_eng}, {right_eng} must hold in the next step"
-    return None
+                if (type(left) is ltlnode.LiteralNode and 
+                    type(right.operand) is ltlnode.LiteralNode and
+                    left.value == right.operand.value):
+                    return None
+                left_eng = clean_for_composition(left.__to_english__())
+                right_eng = clean_for_composition(right.operand.__to_english__())
+                verb = "will hold" if get_pragmatic_policy().avoid_deontic else "must hold"
+                if get_pragmatic_policy().avoid_causal:
+                    return f"if {left_eng}, then {right_eng} {verb} in the next step"
+                return f"whenever {left_eng}, {right_eng} {verb} in the next step"
+    return None
 
 
 ## Bounded Response Pattern  
@@ -553,40 +755,46 @@ def immediate_response_pattern_to_english(node):
 # Source: Dwyer et al. "Patterns in Property Specifications" ICSE 1999
 #         This is a variant of the response pattern with a one-step delay
 @pattern
-def bounded_response_pattern_to_english(node):
+def bounded_response_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.ImpliesNode:
             left = op.left
             right = op.right
             if type(right) is ltlnode.NextNode:
-                inner = right.operand
-                if type(inner) is ltlnode.FinallyNode:
-                    left_eng = clean_for_composition(left.__to_english__())
-                    right_eng = clean_for_composition(inner.operand.__to_english__())
-                    return f"whenever {left_eng}, {right_eng} will eventually occur after the next step"
-    return None
+                inner = right.operand
+                if type(inner) is ltlnode.FinallyNode:
+                    left_eng = clean_for_composition(left.__to_english__())
+                    right_eng = clean_for_composition(inner.operand.__to_english__())
+                    if get_pragmatic_policy().avoid_causal:
+                        return f"if {left_eng}, then {right_eng} will eventually occur after the next step"
+                    return f"whenever {left_eng}, {right_eng} will eventually occur after the next step"
+    return None
 
 
 ## G !p
 # English: It will never be the case that p (holds)
 @pattern
-def never_globally_pattern_to_english(node):
+def never_globally_pattern_to_english(node):
     if type(node) is ltlnode.GloballyNode:
         op = node.operand
         if type(op) is ltlnode.NotNode:
             negated = op.operand
             negated_eng = clean_for_composition(negated.__to_english__())
             # For literals, use simpler phrasing with multiple alternatives
-            if type(negated) is ltlnode.LiteralNode:
-                patterns = [
-                    f"{negated_eng} will never occur",
-                    f"always avoid {negated_eng}",
-                    f"never {negated_eng}",
-                    f"{negated_eng} must never happen"
-                ]
-                return choose_best_sentence(patterns)
-            return f"it is never the case that {negated_eng}"
+            if type(negated) is ltlnode.LiteralNode:
+                patterns = _deontic_variants(
+                    [
+                        f"{negated_eng} will never occur",
+                        f"always avoid {negated_eng}",
+                        f"never {negated_eng}"
+                    ],
+                    [
+                        f"{negated_eng} must never happen"
+                    ]
+                )
+                return choose_best_sentence(patterns)
+            return f"it is never the case that {negated_eng}"
 
 
 #### Finally special cases ####
@@ -777,7 +985,7 @@ def not_finally_pattern_to_english(node):
 # This means: it's not always the case that !(p & X p), which means
 # eventually p & X p will happen, indicating p holds in consecutive steps
 @pattern  
-def recovery_pattern_to_english(node):
+def recovery_pattern_to_english(node):
     """Detect and translate the recovery pattern !G(!(p & X p))."""
     # Early return if not a NotNode
     if type(node) is not ltlnode.NotNode:
@@ -807,14 +1015,18 @@ def recovery_pattern_to_english(node):
             left.value == right.operand.value):
         return None
     
-    # Pattern matched! Provide alternative phrasings
-    lit_eng = clean_for_composition(left.__to_english__())
-    patterns = [
-        f"{lit_eng} should eventually hold in consecutive steps, with a grace period for recovery",
-        f"{lit_eng} must eventually occur in back-to-back steps, allowing for recovery",
-        f"{lit_eng} will eventually happen consecutively, with recovery allowed"
-    ]
-    return choose_best_sentence(patterns)
+    # Pattern matched! Provide alternative phrasings
+    lit_eng = clean_for_composition(left.__to_english__())
+    patterns = _deontic_variants(
+        [
+            f"{lit_eng} will eventually happen consecutively, with recovery allowed"
+        ],
+        [
+            f"{lit_eng} should eventually hold in consecutive steps, with a grace period for recovery",
+            f"{lit_eng} must eventually occur in back-to-back steps, allowing for recovery"
+        ]
+    )
+    return choose_best_sentence(patterns)
 
 
 ### Until special cases ###
@@ -897,7 +1109,7 @@ def next_until_pattern_to_english(node):
 
 # Pattern: (p U q) | G p  -- weak until phrasing
 @pattern
-def weak_until_disjunction_pattern_to_english(node):
+def weak_until_disjunction_pattern_to_english(node):
     if type(node) is ltlnode.OrNode:
         left, right = node.left, node.right
 
@@ -905,15 +1117,15 @@ def match(until, glob):
             if type(until) is ltlnode.UntilNode and type(glob) is ltlnode.GloballyNode:
                 p, q = until.left, until.right
                 if ltlnode.LTLNode.equiv(str(p), str(glob.operand)):
-                    p_eng = clean_for_composition(p.__to_english__())
-                    q_eng = clean_for_composition(q.__to_english__())
-                    return choose_best_sentence([
-                        # Canonical: explicit case split
-                        f"{p_eng} holds until {q_eng} happens, or {p_eng} holds forever if {q_eng} never happens",
-                        # Template B: conditional termination
-                        f"{p_eng} keeps holding and stops only if {q_eng} happens",
-                    ])
-            return None
+                    p_eng = clean_for_composition(p.__to_english__())
+                    q_eng = clean_for_composition(q.__to_english__())
+                    patterns = [
+                        f"{p_eng} holds until {q_eng} happens, or {p_eng} holds forever if {q_eng} never happens"
+                    ]
+                    if not get_pragmatic_policy().explicit_weak_until:
+                        patterns.append(f"{p_eng} keeps holding and stops only if {q_eng} happens")
+                    return choose_best_sentence(patterns)
+            return None
 
         # Handle (p U q) ∨ G p and G p ∨ (p U q)
         return match(left, right) or match(right, left)
diff --git a/src/stepper.py b/src/stepper.py
index 3815040..cded48b 100644
--- a/src/stepper.py
+++ b/src/stepper.py
@@ -27,7 +27,7 @@ def getLTLFormulaAsString(node, syntax):
     elif syntax == "English":
         ## We should hopefully never get here. However, 
         ## I'm adding it here to suggest a way forward.
-        return ltltoeng.finalize_sentence(node.__to_english__())
+        return ltltoeng.translate(node, discourse=True)
 
     ## Default to classic syntax
     return str(node)