Explaining modal logic proofs

The authors present a technique for the generation of text explanations for proofs in modal logic. These explanations were generated from structures corresponding to Gentzen style proofs in a modified sequent system. Proofs in this system were represented by a recursive term structure, and natural-language explanations generated by a simple mapping from these term structures to text strings. The authors discuss the X proof system, a tactic-style theorem-proving system for first-order logic with a collection of inference rules corresponding to human-oriented proof techniques. They focus on the extension of X to incorporate proofs in modal logic, and on the different kinds of explanations of modal proofs that can be produced to meet the needs of different users.