We propose a proof representation format for human-oriented proofs at the assertion level with underspecification. This work aims at providing a possible solution to challenging phenomena worked out in empirical 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.
['Serge Autexier', 'Christoph Benzmüller', 'Armin Fiedler', 'Helmut Horacek', 'Bao Quoc Vo']
Assertion-level Proof Representation with Under-Specification