next up previous contents index
Next: Theorem Proving Up: Research Topics Previous: Methodology and Verification


The editing facilities of this system were inspired in part by those of the Cornell  Program Synthesizer [Teitelbaum & Reps 81] and by AVID [Krafft 81] , the system which first applied these ideas in the setting of proof synthesis. We have been using these editors in the   system since 1983. We know how to use them effectively, and while we have not seen demonstrated a better way of generating proofs, based on our experience with these systems we now understand feasible ways to improve them significantly. Research on this topic is under way in our group.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995