How do you correctly reason that this directed graph is acyclic?

A more general approach to this is given by topological sorting. In particular, a topological sort exists if and only if the graph is a directed acyclic graph. The 'algorithms' described in the other answers effectively perform a topological sort, in that they repeatedly remove vertices with no incoming/outgoing edges.

For instance, a topological ordering of your graph is given by $A,B,C,D,E,F$ and if you redraw the graph so that the earlier vertices are higher than later vertices (not necessarily linearly) you can see that there are no 'upward' edges, so there can be no cycle.

Step 1. Since $A$ has no indegree it can't be part of any cycle. So remove it. We have now graph $G_1$.

Step 2. Since $C$ has no indegree it can't be part of any cycle (in this new graph $G_1$). So remove it. We get $G_2$

Step 3. Now in $G_2$ nodes $B$ and $D$ have no indegree so remove them.

A directed cycle can't involve $F$ since no arrows start from $F$. So you can delete $F$ and all arrows that land at $F$ from the graph. The original graph is acyclic if and only if the new graph is.

Repeat the procedure with $E$ now. Then with $D$, then with $B$ and $C$.

In the end, only $A$ remains, with no edges, that is an acyclic graph.

As B. Mehta's answer indicates, you can solve this problem in the general case by topo-sorting. Here's a quick guide to how to do that:

• Start by coloring every node green.

Now do the following steps for every node:

• If the node is red, skip it. We've already checked it for cycles.
• If the node is yellow, you've got a cycle. We're done.
• The node must be green. Recolor it yellow.
• Re-start this algorithm for all the outgoing neighbours of the current node.
• When they're all done, color this node red.

Once you're done that, either you encountered a yellow node, or you did not. If you did not, there is no cycle. If you did, then there is a cycle, and it contains the yellow node.

Let's look at your example. We start with everything green. Let's suppose that we're going to look at the nodes in order A, B, C, D, E, F.

A becomes yellow. We must now look at B, C, D next.
  B becomes yellow. We must look at E next.
    E becomes yellow. We must look at F next.
      F becomes yellow.
      F becomes red. 
    E becomes red.
  B becomes red.
  C becomes yellow. We must look at F next.
    F is red, so we skip it.
  C becomes red.
  D becomes yellow. We must look at E and F next.
    But they are both red, so skip them.
  D becomes red.
  A becomes red.
B, C, D, E and F are all red, so we're done, and the graph is acyclic.

Now suppose we have A -> B -> C -> A. They're all green.

A becomes yellow; we have to look at B next.
  B becomes yellow; we have to look at C next.
    C becomes yellow; we have to look at A next.
      A is yellow. There is a cycle.

Make sense?

Bonus algorithm: Suppose the graph is acylic. When you color a node red, put an increasing number on it. In our example, F = 1, E = 2, B = 3, C = 4, D = 5 A = 6. If you removed the nodes from the graph in that order, you would never remove a node that had an outbound edge.

That's why this is called "topological sort". It lets us find an order on a DAG where an arrow pointing from A to B means "task A cannot be done until after task B is done". In our example, F has to be done first, and sure enough, it is. We remove F from the graph, and now E has to be done next. We remove E from the graph and now B, C or D are equally good so we can do them, and then we must do A last.