Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Call for Papers: THedu'11 (Postproceedings)
Posted:
Sep 1, 2011 11:17 AM


[Apologies for possible multiple postings.]
 Call for Papers PostProceedings  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 nextgeneration 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, ATPsystems 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 ITPSystems, in particular those following the LCFprover 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 enquirybased 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.
* UserGuidance 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 userguidance 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 userguidance 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  RalphJohan 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 ParisSud, France Burkhart Wolff, University ParisSud, France
Submission 
The postproceedings 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 1014 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 postproceedings paper (it won't be considered in that case), but instead make sure to submit your postproceedings 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 P3001454 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



