# [DOUBT] Translation of Logic to CTL

Hello!. I am trying to solve this logic translation to CTL, as given in the solutions of the paper, dated 2021.02.17.

In the 2nd step, F[d U b] was converted to FGd | Fb. But in the next step, AGd is written with a note at the bottom. Could anyone please explain how the reduction took place from step 2 to 3.?.

The claim is that (Gd & (FGd | Fb)) is equivalent to Gd. To see this, note first that Gd implies FGd since Gd demands that always d holds, and hence, it then holds also after any other point of time forever. Now, abbreviate p:=Gd, q:=FGd and r:=Fb and note finally that the following propositional logic formula is valid:

(p->q) -> (p & (q | r) <-> p)
by (166k points)
selected by
Thank you for the explanation. I get the idea now.

Just to confirm my understanding, would it be true if there is a formula in the given format: Gd & (FGd | <any path formula or state formula>), for example:

Gd & (FGd | GFa) or Gd & (FGd | [d U b])

The rule of (p->q) -> (p & (q | r) <-> p) would still apply?
Yes, it does still apply. As you wrote above the second formula in the disjunction can be any formula.
Thanks for the clarification.