  The proposed approach is to formalise the probabilistic puzzle in equational
FOL. Two formalisations are needed: one theory for all models of the given
puzzle, and a second theory for the favorable models. Then Mace4 - that
computes all the interpretation models of a FOL theory - is called twice.
First, it is asked to compute all the possible models M p .Second, the
additional constraint is added, and Mace4 computes only favourabile models M f.
Finally, the definition of probability is applied: the number of favorable
models is divided by the number of possible models. The proposed approach
equips students from the logic tribe to find the correct solution for puzzles
from the probabilitistic tribe, by using their favourite instruments: modelling
and formalisation. I have exemplified here five probabilistic puzzles and how
they can be solved by translating the min FOL and then find the corresponding
interpretation models. Mace4 was the tool of choice here. Ongoing work is
investigating the limits of this method on various collections of probabilistic
puzzles
