Call for Papers: THedu'11 at CADE-23

[Walther Neuper]

[Apologies for possible multiple postings.]
----------------------------------------------------------------------
                             CALL FOR PAPERS
----------------------------------------------------------------------
                                THedu'11
                 CTP components for educational software
                   http://www.uc.pt/en/congressos/thedu

                           Workshop at CADE-23,
           23nd International Conference on Automated Deduction
                 Wroclaw, Poland, July 31- August 5, 2011
                       http://cade23.ii.uni.wroc.pl/
----------------------------------------------------------------------

THedu'11 Scope
--------------
This workshop intends to gather the research communities for Computer 
Theorem proving (CTP), 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 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 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 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 enquiry-based learning 
from concrete to abstract --- and the knowledge's logical coherence 
supports such learning: for instance, the formula 2.π 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 tracable 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, use 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 MMAs which are interactive and which explain 
themselves such that interested students can independently learn by 
inquiry and experimentation.


Program Committee
-----------------
   Ralph-Johan Back, Abo University, Turku, Finland
   Francisco Botana, University of Vigo at Pontevedra, Spain
   Florian Haftman, Munich University of Technology, Germany
   Predrag Janicic, University of Belgrade, Serbia
   Cezary Kaliszyk, University of Tsukuba, Japan
   Julien Narboux, University of Strasbourg, France
   Walther Neuper, Graz University of Technology, Austria
   Pedro Quaresma, University of Coimbra, Portugal
   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

Important Dates
---------------
   * Abstract Submission:  15 Apr 2011
   * Submission Deadline:  29 Apr 2011 (by THedu'11 easychair)
   * Author Notification:   3 Jun 2011
   * Final Version:         1 Jul 2011 (by THedu'11 easychair)
   * Worshop Day:          31 Jul 2011

Submission
----------
We welcome submission of proposals to present a demo, as well as 
submissions of papers presenting original unpublished work which is not 
been submitted for publication elsewhere.

Selected papers will appear in CISUC Technical Report series (ISSN 
0874-338X, [1]). All accepted papers and system demos will be presented 
at the workshop, and the extended abstracts will be made available 
online. A publication medium for post-proceedings is under consideration.

Papers and demo proposals should be submitted via THedu'11 easychair [2].

Papers should be no more than 8 pages in length and are to be submitted 
in PDF format. They must conform to the ACM SIGPLAN style guidelines [3].

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

[1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/
[2] http://www.easychair.org/conferences/?conf=thedu11
[3] http://www.acm.org/sigs/sigplan/authorInformation.htm