Assertion-level Proof Representation with Under-Specification
Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek, Vo Nguyen Quoc Bao · Electronic Notes in Theoretical Computer Science · 2004
We propose a proof representation format for human-oriented proofs at the assertion level with under-specification. This work aims at providing a possible solution to challenging phenomena worked out in em-pirical studies in the Dialog project at Saarland University. A particular challenge in this project is to bridge the gap between the human-oriented proof representation format with under-specification used in the proof manager of the tutorial dialogue system and the calculus- and machine-oriented representation format of the domain reasoner.