CALL FOR PARTICIPATION
----------------------------------------------------------------------
THedu'11
CTP components for educational software
=======================================
(CTP -- Computer Theorem Proving)
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 program: http://www.uc.pt/en/congressos/thedu/schedule
----------------
THeud'11 proceedings: http://www.uc.pt/en/congressos/thedu/proceedings
--------------------
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 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 Haftmann, 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
--
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: [log in to unmask]
p\'agina: http://www.mat.uc.pt/~pedro/
telef: +351 239 791 137; fax: +351 239 832 568
