We describe an environment that allows the users of the Theorema system to flexibly control aspects of computer-supported proof development. The environment supports the display and manipulation of proof trees and proof situations, logs the user activities (commands communicated with the system during the proving session), and presents (also unfinished) proofs in a human-oriented style. In particular, the user can navigate through the proof object, expand/remove proof branches, provide witness terms, develop several proofs concurrently, proceed step by step or automatically and so on. The environment enhances the effectiveness and flexibility of the reasoners of the Theorema system. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Piroi, F., & Kutsia, T. (2005). The theorema environment for interactive proof development. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 261–275). https://doi.org/10.1007/11591191_19
Mendeley helps you to discover research relevant for your work.