Presenting machine-found proofs. This paper outlines an implemented system named PROVERB that transforms and abstracts machine-found proofs to natural deduction style proofs at an adequate level of abstraction and then verbalizes them in natural language. The abstracted proofs, originally employed only as an intermediate representation, also prove to be useful for proof planning and proving by analogy.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Fehrer, Detlef; Horacek, Helmut: Presenting inequations in mathematical proofs (1999)
- Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg; Sorge, Volker: (\Omega)\textscmega: towards a mathematical assistant (1997)
- Huang, Xiaorong; Fiedler, Armin: Presenting machine-found proofs (1996)