Our Approach
Basic Principle: Semantic choices about the proof text can be based on information provided by the theorem prover.
The high-level proof structure is used for discourse planning.
Sentence content can be determined from the type of inference being made.