The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 19 of 397
Back to Result List

The Presentation of Proofs at the Assertion Level

  • Most automated theorem provers suffer from the problem that theycan produce proofs only in formalisms difficult to understand even forexperienced mathematicians. Efforts have been made to transformsuch machine generated proofs into natural deduction (ND) proofs.Although the single steps are now easy to understand, the entire proofis usually at a low level of abstraction, containing too many tedioussteps. Therefore, it is not adequate as input to natural language gen-eration systems.To overcome these problems, we propose a new intermediate rep-resentation, called ND style proofs at the assertion level . After illus-trating the notion intuitively, we show that the assertion level stepscan be justified by domain-specific inference rules, and that these rulescan be represented compactly in a tree structure. Finally, we describea procedure which substantially shortens ND proofs by abstractingthem to the assertion level, and report our experience with furthertransformation into natural language.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Xiaorong Huang
URN:urn:nbn:de:hbz:386-kluedo-3162
Series (Serial Number):SEKI Report (93,4)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of first Publication:1999
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011