[TYPES/announce] last CfA "TP components for educational software" at CICM

[Walther Neuper]

deadline 6.May
---------------------------------------------------------------------
                        Last Call for Extended Abstracts
----------------------------------------------------------------------
                                   THedu'13
                     TP components for educational software
                     ======================================
                     (http://www.uc.pt/en/congressos/thedu)
                                 Wednesday, 10.July

                              Co-located with CICM 2013
                   Conferences on Intelligent Computer Mathematics
                                     Bath, UK
                  http://www.cicm-conference.org/2013/cicm.php
----------------------------------------------------------------------

THedu'13 Scope
--------------

THedu is a forum to gather the research communities for computer
Theorem Proving (TP), Automated Theorem Proving (ATP), Interactive
Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS)
and Dynamic Geometry Systems (DGS).
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.

Important Dates:
---------------

      * Extended Abstracts:     06 May 2013
      * Author Notification:    03 Jun 2013
      * Final Version:          15 Jun 2013
      * Workshop Day:           (still to be defined, 8-12 July)
      * Postproceedings(EPTCS): 15 October 2013

(https://www.easychair.org/conferences/?conf=thedu13)

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
   postconditions 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 specialized 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 Stepwise 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, CTP 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!

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.

Submission
----------

We welcome submission of extended abstracts (4 pages max) presenting
original unpublished work which is not been submitted for publication
elsewhere.

All accepted extended abstracts will be presented at the workshop, and
the extended abstracts will be made available online. A publication
post-proceedings (papers, 16 pages max) under EPTCS is under
consideration.

Extended abstracts and demo proposals should be submitted via THedu'13
easychair (https://www.easychair.org/conferences/?conf=thedu13).

Extended abstracts should be no more than 4 pages in length and are to
be submitted in PDF format. They must conform to the EPTCS style
guidelines (http://http://style.eptcs.org/).

At least one author of each accepted extended abstract/demo is
expected to attend THedu'13 and presents her or his extended
abstract/demo.

Program Committee
-----------------
      Ralph-Johan Back, Abo Akademy University, Finland
      Francisco Botana, University of Vigo at Pontevedra, Spain
      Roman Hašek, University of South Bohemia
      Predrag Janicic, University of Belgrade, Serbia
      Julien Narboux, University of Strasbourg, France
      Filip Maric, University of Belgrade, Serbia
      Walther Neuper, Graz University of Technology, Austria
      Pavel Pech, University of South Bohemia
      Vanda Santos, CISUC, Portugal
      Wolfgang Schreiner, University of Linz, Austria
      Dusan Vallo, University of Nitra, Slovakia
      Makarius Wenzel, University Paris-Sud, France
      Burkhart Wolff, University Paris-Sud, France