ThEdu'14 - Theorem Provers Components for Educational Software
ThEdu'14 Web-page
THedu is a forum to gather the research communities for Automated
Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as
for Computer Algebra Systems (CAS), Dynamic Geometry Systems (DGS)
and Mathematical Education. The goal of this union is to combine and
focus systems of these areas and to enhance existing educational
software as well as studying the design of the next generation of
mechanised mathematics assistants.
Elements for next-generation assistants include:
- Declarative Languages for Problem Solution: education in applied
sciences and in engineering is mainly concerned with problems, which
are understood as operations on elementary objects to be transformed
to an object representing a problem solution. Preconditions and
post-conditions of these operations can be used to describe the
possible steps in the problem space; thus, ATP-systems can be used
to check if an operation sequence given by the user does actually
present a problem solution. Such "Problem Solution Languages"
encompass declarative proof languages like Isabelle/Isar or Coq's
Mathematical Proof Language, but also more specialised forms such
as, for example, geometric problem solution languages that express a
proof argument in Euclidean Geometry or languages for graph theory.
- Consistent Mathematical Content Representation: libraries of
existing ITP-Systems, in particular those following the LCF-prover
paradigm, usually provide logically coherent and human readable
knowledge. In the leading provers, mathematical knowledge is covered
to an extent beyond most courses in applied sciences. However, the
potential of this mechanised knowledge for education is clearly not
yet recognised adequately: renewed pedagogy calls for enquiry-based
learning from concrete to abstract --- and the knowledge's logical
coherence supports such learning: for instance, the formula 2.Pi
depends on the definition of reals and of multiplication; close to
these definitions are the laws like commutativity etc. Clearly, the
complexity of the knowledge's traceable interrelations poses a
challenge to usability design.
- User-Guidance in Step-wise Problem Solving: Such guidance is
indispensable for independent learning, but costly to implement so
far, because so many special cases need to be coded by
hand. However, TP technology makes automated generation of
user-guidance reachable: declarative languages as mentioned above,
novel programming languages combining computation and deduction,
methods for automated construction with ruler and compass from
specifications, etc --- all these methods 'know how to solve a
problem'; so, using the methods' knowledge to generate user-guidance
mechanically is an appealing challenge for ATP and ITP, and probably
for compiler construction.
- Pedagogical strategies: Using TP technologies in learning
environments call for strategies for linking and adapting the
availble tools for specific educational needs and new methods for
the management of mathematical knowledge capable of filling the gap
between repositories and end-user system and new visual and/or
natural language interfaces to allow the use of rigorous reasoning
methods and tools.
In principle, mathematical software can be conceived as models of
mathematics: The challenge addressed by this workshop is to provide
appealing models for mathematics assistants which are interactive
and which explain themselves such that interested students can
independently learn by inquiry and experimentation.
Programme Committee
- Francisco Botana, University of Vigo at Pontevedra, Spain
- Roman HaĊĦek, University of South Bohemia, Czech Republic
- Filip Maric, University of Belgrade, Serbia
- Walther Neuper, Graz University of Technology, Austria (co-chair)
- Pedro Quaresma, University of Coimbra, Portugal (co-chair)
- Vanda Santos, CISUC, Portugal
- Wolfgang Schreiner, Johannes Kepler University, Austria
|
