TREE-ORIENTED INTERACTIVE PROCESSING WITH AN APPLICATION TO THEOREM-PROVING.

The concept of 'unstructured structure editing' and ted, an editor for unstructured trees, are described. Ted is used to manipulate hierarchies of information in an unrestricted manner. The tool was implemented and applied to the problem of organizing formal proofs. As a proof management tool, it maintains the validity of a proof and its constituent lemmas independently from the methods used to validate the proof. It includes an adaptable interface which may be used to invoke theorem provers and other aids to proof construction. Using ted, a user may construct, maintain, and verify formal proofs using a variety of theorem provers, proof checkers, and formatters. A prototype program editor based on these ideas is briefly discussed.