Most automated theorem provers are based on resolution, and produce proofs that are hard to read for a human. I wonder if there are provers which can generate human readable proofs, either in natural language, or in at least in form that is intelligible for humans. I am aware of : A fully automatic problem solver with human-style output M. Ganesalingam, W. T. Gowers Are there any other provers ?
I could not find other references in the above paper.