Granularity-Adaptive Proof Presentation (bibtex)
by Marvin Schiller, Christoph Benzmüller
Abstract:
When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem provers, in contrast, present proofs usually at a fixed level of detail (also called granularity). Often these presentations are neither intended nor suitable for human use. A challenge therefore is to develop user- and goal-adaptive proof presentation techniques that obey common mathematical practice. We present a flexible and adaptive approach to proof presentation that exploits machine learning techniques to extract a model of the specific granularity of proof examples and employs this model for the automated generation of further proofs at an adapted level of granularity.
Reference:
Granularity-Adaptive Proof Presentation (Marvin Schiller, Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), SEKI Working-Paper SWP--2009--01, 2009. (arXiv:0903.0314)
Bibtex Entry:
@techreport{R44,
  Abstract =	 {When mathematicians present proofs they usually
                  adapt their explanations to their didactic goals and
                  to the (assumed) knowledge of their
                  addressees. Modern automated theorem provers, in
                  contrast, present proofs usually at a fixed level of
                  detail (also called granularity). Often these
                  presentations are neither intended nor suitable for
                  human use. A challenge therefore is to develop user-
                  and goal-adaptive proof presentation techniques that
                  obey common mathematical practice. We present a
                  flexible and adaptive approach to proof presentation
                  that exploits machine learning techniques to extract
                  a model of the specific granularity of proof
                  examples and employs this model for the automated
                  generation of further proofs at an adapted level of
                  granularity.},
  Institution =	 {Saarland University},
  Address =	 {{DFKI Bremen GmbH, Safe and Secure Cognitive
                  Systems, Cartesium, Enrique Schmidt Str.\,5,
                  D--28359 Bremen, Germany}},
  Author =	 {Schiller, Marvin and Benzm{\"u}ller, Christoph},
  Keywords =	 {own, Proof Presentation, DIALOG, Natural Language Dialog,
                  Proof Assistants, Machine Learning, Tutoring
                  Systems},
  Note =	 {arXiv:0903.0314},
  Publisher =	 {{SEKI Publications (ISSN 1437-4447)}},
  Series =	 {{SEKI Working-Paper SWP--2009--01}},
  Title =	 {Granularity-Adaptive Proof Presentation},
  Url =		 {http://arxiv.org/abs/0903.0314},
  Year =	 2009,
}
Powered by bibtexbrowser