Enconding a Hierarchical Proof Data Structure for Contextual Reasoning in a Logical Framework
Syed Sajjad Hussain, Jörg Siekmann, Christoph Benzmüller · MPG.PuRe (Max Planck Society) · 2005
For many application such as mathematical assistant systems, an effective communication between the system and its users is critical for the acceptance of a system. Explaining the computer-supported proofs in natural language can enhance the understanding of the users. We define a function that encodes the proofs generated from the computer-supported theorem proving system MEGA into TWEGA, which is the input language of the proof presentation system P.rex. This encoding enables the natural language explanation of MEGA proofs in P.rex