Summary
The high-level nature of a tactic-style proof allows effective and efficient:
- determination of the high-level structure of a proof text
- division of proof information into sentence objects
Generation framework described is receptive to improvements in accomplishing the above tasks:
- Improved models for human notions of triviality and similarity of reasoning
- Communication between generation system and theorem proving system to fill in background mathematical knowledge