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

David Hammerslag, Samuel N. Kamin, R H Campbell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationUnknown Host Publication Title
PublisherIEEE
Pages199-206
Number of pages8
ISBN (Print)0897911733
StatePublished - Dec 1 1985

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'TREE-ORIENTED INTERACTIVE PROCESSING WITH AN APPLICATION TO THEOREM-PROVING.'. Together they form a unique fingerprint.

Cite this