Enconding a Hierarchical Proof Data Structure for Contextual Reasoning in a 
Logical Framework

Hussain, Syed Sajjad

Lokale TagsFreigabegeschichteDetailsÜbersicht

Enconding a Hierarchical Proof Data Structure for Contextual Reasoning in a Logical Framework

Hussain, S. S. (2005). Enconding a Hierarchical Proof Data Structure for Contextual Reasoning in a Logical Framework. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-D5CB-8 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0028-35D0-4

Genre: Hochschulschrift

ausblenden:

Urheber:
Hussain, Syed Sajjad^{1, 2}, Autor
Siekmann, Jörg³, Ratgeber
Benzmüller, Christoph³, Gutachter

Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045
3External Organizations, ou_persistent22

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: 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