PROVERB swMATH ID: 29672 Software Authors: Huang, Xiaorong; Fiedler, Armin Description: 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. Homepage: https://link.springer.com/chapter/10.1007%2F3-540-61511-3_83 Keywords: natural deduction; intermediate representation; mathematical textbook; linguistic resource; resolution proof Related Software: Omega-MKRP; OTTER; OMEGA; IMPS; KQML; Lambda-Clam; InKa; Analytica; VSDITLU; MBase; OMDoc; Automath; Oz; ETPS; Isabelle/ZF; OMRS; TPS Cited in: 4 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Presenting machine-found proofs. Zbl 1412.68235Huang, Xiaorong; Fiedler, Armin 1996 all top 5 Cited by 15 Authors 2 Fehrer, Detlef 2 Fiedler, Armin 2 Huang, Xiaorong 2 Kohlhase, Michael 1 Benzmüller, Christoph Ewald 1 Cheikhrouhou, Lassaad 1 Franke, Andreas 1 Horacek, Helmut 1 Kerber, Manfred 1 Konrad, Karsten 1 Meier, Andreas 1 Melis, Erica 1 Schaarschmidt, Wolf 1 Siekmann, Jörg H. 1 Sorge, Volker Cited in 2 Serials 1 Information Sciences 1 Journal of Symbolic Computation Cited in 2 Fields 4 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year