非表示:
キーワード:
-
要旨:
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
