de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

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

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44659

Hussain,  Syed Sajjad
International Max Planck Research School, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0027-D5CB-8
Abstract
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