Proof Annotations

Much research work in the area of theorem provers has been concerned with improving interaction with provers, but usually at the level of mouse-and-window based interaction. In reality, the human-guided process of developing informal proofs has not been properly interfaced to formal machine-based proofs, and informal knowledge and hints about the nature of a problem domain have neither been captured nor exploited to help the proof effort. The research being proposed here addresses this problem, by formulating a mechanism by which existing general-purpose interactive theorem provers can be extended to handle domain- and problem-specific information.

We are looking at ways to add extra-formal information to theorem-provers.

Staff involved: Sara Kalvala