Call for Papers: THedu'11 (Post-proceedings)

Do Sep 1 17:20:15 CEST 2011

[Apologies for possible multiple postings.]

----------------------------------------------------------------------
                     Call for Papers Post-Proceedings
----------------------------------------------------------------------
				THedu'11
		CTP components for educational software
		=======================================
		   (CTP -- Computer Theorem Proving)
                  http://www.uc.pt/en/congressos/thedu
----------------------------------------------------------------------

Important Dates
---------------
 * Call for papers:             1.Sep.2011
 * Submission (full papers):   15.Nov.2011
 * Notification of acceptance: 15.Dec.2011
 * Revised papers due:         15.Jan.2012
----------------------------------------------------------------------

THedu is a forum 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
and 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 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 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 University, Turku, Finland
 Pedro Quaresma, University of Coimbra, Portugal

Program Committee
 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
 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
----------

The post-proceedings of THedu'11 will be published in the Electronic
Proceedings in Theoretical Computer Science (EPTCS) series. You are
invited to submit original research papers (of 10-14 pages) for
possible publication in the proceedings. Your contributions have to be
within the scope of THedu, but their contents do not have to be related
to a past presentation at THedu'11. Submissions which do not have been
presented at THedu'11 are welcome.

All the submissions will be formally reviewed according to the usual
standard of international conferences. The proceedings will be edited
by the PC chairs.

THedu'11 seeks papers presenting original unpublished work which is
not been submitted for publication elsewhere.

Submission guidelines 
---------------------

The authors of papers should submit to easychair in PDF format
generated by EPTCS LaTeX style(*).

We will use the same submission page as for the workshop:

  http://www.easychair.org/conferences/?conf=thedu11

Do NOT UNDER ANY CIRCUMSTANCES replace your workshop submission by
your new post-proceedings paper (it won't be considered in that case),
but instead make sure to submit your post-proceedings contribution as
a NEW AND INDEPENDENT SUBMISSION.

Please feel free to contact us if you have any comments, suggestions,
and/or questions. We look forward to receiving your submissions.

With best wishes,

The Program Committee of THedu'11

(*) http://www.cse.unsw.edu.au/~rvg/EPTCS/eptcsstyle.zip

-- 
  At\'e breve;\`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 at mat.uc.pt
p\'agina: http://www.mat.uc.pt/~pedro/
telef: +351 239 791 137; fax: +351 239 832 568