Date: Feb 27, 2013 10:24 AM Author: pedro@mat.uc.pt Subject: ThEdu'13 - call for papers --------------------------------------------------------------------

Call for Papers

----------------------------------------------------------------------

THedu'13

TP components for educational software

(http://www.uc.pt/en/congressos/thedu)

Co-located with CICM 2013

Conferences on Intelligent Computer Mathematics

8.-12. July 2013

Bath, UK

http://www.cicm-conference.org/2013/cicm.php

----------------------------------------------------------------------

THedu'13 Scope

--------------

THedu is a forum to gather the research communities for computer

Theorem Proving (TP), 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.

Important Dates:

---------------

* Extended Abstracts: 06 May 2013

* Author Notification: 03 Jun 2013

* Final Version: 15 Jun 2013

* Workshop Day: (still to be defined, 8-12 July)

* Postproceedings(EPTCS): 15 October 2013

(https://www.easychair.org/conferences/?conf=thedu13)

Elements for next-generation assistants 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 mathematics assistants which are interactive and

which explain themselves such that interested students can

independently learn by inquiry and experimentation.

Submission

----------

We welcome submission of extended abstracts (4 pages max) presenting

original unpublished work which is not been submitted for publication

elsewhere.

All accepted extended abstracts will be presented at the workshop, and

the extended abstracts will be made available online. A publication

post-proceedings (papers, 16 pages max) under EPTCS is under

consideration.

Extended abstracts and demo proposals should be submitted via THedu'13

easychair (https://www.easychair.org/conferences/?conf=thedu13).

Extended abstracts should be no more than 4 pages in length and are to

be submitted in PDF format. They must conform to the EPTCS style

guidelines (http://http://style.eptcs.org/).

At least one author of each accepted extended abstract/demo is

expected to attend THedu'13 and presents her or his extended

abstract/demo.

Program Committee

-----------------

Ralph-Johan Back, Abo Akademy University, Finland

Francisco Botana, University of Vigo at Pontevedra, Spain

Roman Ha?ek, University of South Bohemia

Predrag Janicic, University of Belgrade, Serbia

Julien Narboux, University of Strasbourg, France

Filip Maric, University of Belgrade, Serbia

Walther Neuper, Graz University of Technology, Austria

Pavel Pech, University of South Bohemia

Vanda Santos, CISUC, Portugal

Wolfgang Schreiner, University of Linz, Austria

Dusan Vallo, University of Nitra, Slovakia

Makarius Wenzel, University Paris-Sud, France

Burkhart Wolff, University Paris-Sud, France

_________________________________________

--

At\'e breve;Deica Logo;\`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