Four men seated in a boat puzzle I am looking for an elegant way to solve this rather simple logic puzzle using mathematical logic (statements, conjunctions, disjunctions, implications, tautologies, predicate logic and so on). I am not looking for a solution using combinations, variations or permutations, as I have already solved it using that method (given below).
The puzzle is:

Four men (A, B, C, D) should be seated in a boat forming a line. Can you determine the order in which they need to be seated, from the front of the boat to the back, so that all of their requests are satisfied?
Requests:
Man A: I want to be seated at one end of the boat (either first or
  last) only if B sits next to me.
Man B: I don't want to sit next to (either before or after) C and I
  don't want to be last.
Man C: I don't want to sit next to A if I am seated on one end of the
  boat.
Man D: I want to sit next to B or not to sit next to A, and if I am not
  first, then I want to be last (if not seated on the front side, he
  wants to sit at the back side of the boat).

There obviously are $V_{4}^{4}=P_{4} = 4! = 24$ possibilities for this exercise (not sure if the notation is universal), of which only one - "BACD", satisfies the conditions. However, had there been five elements in the example, it wouldn't have been so easy to determine the correct result by experimentation/counting values, which is why I am searching for a logical approach to the problem.
 A: Well, D and B look like they have the most restrictive conditions so we can start with them. Say with D. Suppose D was sat at the front (he can only be first or last). Now suppose we put B second. B cannot sit next to C so C must be last, which makes A third. But then A is next to C so B is unhappy and so this arrangement doesn't work. So now we know that if D is first, B cannot be second. So C has to be second. But now wherever we put B he is unhappy.
Hence we know that D cannot be at the front, so must be at the back. We have now fixed D, so could do some experimenting to find what works (this is now suitable easy since so few combinations exist) but we can keep on purely logically:
As before, suppose B sits next to D. To keep B happy, C must be first and A second, but then C is unhappy. 
So B must not sit next to D. To keep D happy, A must not sit next to D so only C can be third. (Note that at this stage we know that B and C must be arranged as we say, because anything else leads to a contradiction. It is important to distinguish this from where we start by supposing something and then have statements like "C must be first and A second" which were true only if our suppositions were correct.)
All that remains is to say that for B to be happy, he must be first. This leaves A in second place. If we know there is a solution, we do not even need to check that all the conditions hold since we have said that this is the only possible solution. (Note in some cases there may be no solutions, and we would have to check that the only possible solution is actually a solution.)
Also, this was only one way to do it, we could have started by supposing B sat at the back, or by supposing something about where one of the others were sat. It's best to start with the most restrictive condition to save yourself some time, and if you have any intuition about what would happen, make those suppositions first, and then you are more likely to stumble upon the right answer. We find the right one by excluding all others, so the closer we start to correct the quicker we get there!
Edit: With labelling as in the comments, I'll re-write the proof from the point where I said D must be at the back (say D is at 4):
D is at 4. Suppose B is at 3. $P_b \implies $ C is at 1 and hence A is at 2. But then $P_c$ is not satisfied, giving a contradiction.
So B is not at 3. Then $P_d \implies$ A is not at 3. So C is at 3. Now $P_b \implies$ B is at 1. Hence A is at 2. Now $P_a, P_b, P_c, P_d$ are all satisfied so this is the solution.
A: The following seems a useful and consistent way to formalize this problem:
\begin{align}
(a) \quad & A\text{ at end} \;\Rightarrow\; A\text{ next to }B \\
(b1) \quad & \lnot(B\text{ next to }C) \\
(b2) \quad & \lnot(B\text{ at back end}) \\
(c) \quad & C\text{ at end} \;\Rightarrow\; \lnot(A\text{ next to }C) \\
(d1) \quad & B\text{ next to }D \;\lor\; \lnot(A\text{ next to }D) \\
(d2) \quad & \lnot(D\text{ at front end}) \;\Rightarrow\; D\text{ at back end} \\
\end{align}
In addition to these, there are a number of rules about $\;\ldots\text{ next to }\ldots\;$ etc., like $$(0) \quad X\text{ at end} \;\equiv\; X\text{ at front end} \lor X\text{ at back end}$$ but for most of those formalization does not seem helpful.
Now the simplest reasoning I could find is as follows.

First note how $(d2)$ can quickly be simplified to
$$
(d2') \quad D\text{ at end}
$$
by rewriting $\;P \Rightarrow Q\;$ as $\;\lnot P \lor Q\;$ and simplifying using $(0)$.
Since $D$ is at one end by $(d2')$ and there are exactly four seats, we know that $A,B,C$ are sitting next to each other, and more specifically, by $(b1)$, $A$ sits inbetween $B$ and $C$.  Therefore, by $(c)$ and contraposition, $C$ is not at the other end.  Therefore $B$ must be at the other end, and by $(b2)$ that is the front end.
So the conclusion is that $B$ is at the front end, then $A$, then $C$, and finally $D$ at the back end.

Note we did not need to use $(a)$ and $(d1)$.
