UNIVERSITY OF HERTFORDSHIRE
             COMPUTER SCIENCE RESEARCH COLLOQUIUM

                            presents

            "Computer-Assisted Proof Tutoring and the
                 Aspect of Proof Granularity"

                     Dr. Marvin Schiller
                   (Brunel University, UK)

                    6 April 2011  (Wednesday)
                      Meeting Room LD454

                  Hatfield, College Lane Campus
                          1-2  pm

                  Everyone is Welcome to Attend

                  Refreshments will be available

Abstract:



Computer systems for interactive and automated theorem proving can be
used for teaching formal proofs to students. A number of systems have been
built or adapted for this purpose. They provide an opportunity to practice
proof skills by delivering feedback and providing scaffolding and hints.

In this talk, we focus on a dynamic approach to the computer-assisted
teaching of proofs, where the student is intentionally given freedom in
constructing the proof, and it is the system's task to reconstruct the
student's proof attempt and to deliver feedback and suggestions. Three
dimensions of analysis of proof steps (and resp. feedback and suggestions)
are important in this context; correctness, relevance and step size (i.e.,
proof granularity), the latter being the main topic of this talk. We
discuss differences in step size between proofs as they ideally occur in
textbooks and tutorial dialogues, in comparison to computer-generated
proofs. Such discrepancies of computer-generated proofs are considered
detrimental for teaching in the spirit of common mathematical practice. In
view of this, a framework is presented for representing computer-generated
proofs at various granularities, and for aligning these with step
sizes considered acceptable by human teachers. Norms for acceptable
proof granularities can be formulated explicitly, or learned from human
experts via machine learning techniques. This prospect was explored in
an empirical study with human expert teachers.

---------------------------------------------------
Hertfordshire Computer Science Research Colloquium
http://homepages.stca.herts.ac.uk/~nehaniv/colloq