[Thedu] THedu - last call for papers

[Pedro Quaresma <pedro@mat.uc.pt>]

Dear Members of the THedu Interest Group

Looking forward for a fruitful workshop, here it is the last call for papers, 
notice the extended deadline.

----------------------------------------------------------------------
    LAST CALL FOR EXTENDED ABSTRACTS - DEADLINE EXTENSION - 15 May
----------------------------------------------------------------------
                                  THedu'12
                   TP components for educational software
                   =======================================
                      (TP -- Computer Theorem Proving)
                     http://www.uc.pt/en/congressos/thedu

                            Workshop at CICM 2012
                Conferences on Intelligent Computer Mathematics
                              9.-14. July 2012
                   Jacobs University, Bremen, Germany
            http://www.informatik.uni-bremen.de/cicm2012/cicm.php

----------------------------------------------------------------------
Important Dates
---------------
     * Extended Abstracts/Demo proposals 15 May 2012 (extended deadline)
     * Author Notification:              01 Jun 2012
     * Final Version:                    15 Jun 2012 
     * Worshop Day:                      11 Jul 2012
     * Full papers (post-proceedings):   31 Jul 2012 (LaTeX,easychair[2])

THedu'12 Scope
--------------

This workshop intends 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 workshop tries to combine and
focus systems of these areas to enhance existing educational software
as well as studying the design of the next generation of mechanised
mathematics assistants (MMA). Elements for next-generation MMA's
include:

    * Declarative Languages for Problem Solution: education in applied
      sciences and in engineering is mainly concerned with problems,
      which involve 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 Euklidian 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 inquiry-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. However, 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, 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, use the methods' knowledge to generate user-guidance
      mechanically, this 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 series is to
provide appealing models for MMAs which are interactive and which
explain themselves such that interested students can independently
learn by inquiry and experimentation.

Program Chairs
--------------
     Ralph-Johan Back, Abo Akademi University, Finland
     Pedro Quaresma, University of Coimbra, Portugal

Program Committee
     Francisco Botana, University of Vigo at Pontevedra, Spain
     Florian Haftmann, Munich University of Technology, Germany
     Predrag Janicic, University of Belgrade, Serbia
     Cezary Kaliszyk, University of Tsukuba, Japan
     Julien Narboux, University of Strasbourg, France
     Filip Maric, University of Belgrade, Serbia
     Walther Neuper, Graz University of Technology, Austria
     Wolfgang Schreiner, Johannes Kepler University, Linz, Austria
     Laurent Théry, Sophia Antipolis, INRIA, France
     Makarius Wenzel, University Paris-Sud, France
     Burkhart Wolff, University Paris-Sud, France

Submission
----------
THedu'12 seeks papers and demos presenting original unpublished work 
which is not been submitted for publication elsewhere.

Both, papers and demos, are submitted as extended abstracts first,
which must not exceed five pages. The abstract should be new  
material. Demos should be accompanied by links to demos/downloads and 
[existing] system descriptions. Availability of such accompanying 
material will be a strong prerequisite for acceptance.

The authors of the extended abstracts and system descriptions should
submit to easychair [2] in PDF format generated by EPTCS LaTeX style
[3]. Selected extended abstracts and system descriptions will appear
in CISUC Technical Report series (ISSN 0874-338X, [1]).

At least one author of each accepted paper/demo is expected to attend 
THedu'11 and to present her or his paper/demo, and the extended 
abstracts will be made available online.

After presentation at the conference selected authors will be invited to 
submit a substantially revised version, extended to 10-14 pages, for 
publication by the Electronic Proceedings in Theoretical Computer 
Science (EPTCS). Papers/system descriptions will be reviewed by blind 
peer review and evaluated by three referees with respect to relevance, 
clarity, quality, originality, and impact.

Revised versions are submitted in LaTeX according to the EPTCS style 
guidelines [3] via easychair [2].

[1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/
[2] http://www.easychair.org/conferences/?conf=thedu11
[3] http://http://style.eptcs.org/

-- 
  At\'e breve;Deica Logo;\`A bient\^ot;See you later;Vidimo se;

Professor Auxiliar Pedro Quaresma
Departamento de Matem\'atica, Faculdade de Ci\^encias e Tecnologia
Universidade de Coimbra
P-3001-454 COIMBRA, PORTUGAL
correioE: pedro@mat.uc.pt
p\'agina: http://www.mat.uc.pt/~pedro/
telef: +351 239 791 137; fax: +351 239 832 568