  Teaching logic effectively requires an understanding of the factors which
cause logic students to struggle. Formalization exercises, which require the
student to produce a formula corresponding to the natural language sentence,
are a good candidate for scrutiny since they tap into the students'
understanding of various aspects of logic. We correlate the difficulty of
formalization exercises predicted by a previously proposed difficulty
estimation algorithm with two empirical difficulty measures on the Grade
Grinder corpus, which contains student solutions to FOL exercises. We obtain a
moderate correlation with both measures, suggesting that the said algorithm
indeed taps into important sources of difficulty but leaves a fair amount of
variance uncaptured. We conduct an error analysis, closely examining exercises
which were misclassified, with the aim of identifying additional sources of
difficulty. We identify three additional factors which emerge from the
difficulty analysis, namely predicate complexity, pragmatic factors and
typicality of the exercises, and discuss the implications of automated
difficulty estimation for logic teaching and explainable AI.
