Date: Jul 8, 2011 7:06 AM Author: pedro@mat.uc.pt Subject: CALL FOR PARTICIPATION - THedu'11 CTP components for educational software 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: pedro@mat.uc.pt

p\'agina: http://www.mat.uc.pt/~pedro/

telef: +351 239 791 137; fax: +351 239 832 568