[Thedu] 2nd Call for papers

[Pedro Quaresma <pedro@mat.uc.pt>]

Dear THeduers

Below the THedu'12 2nd call for papers, 

Please broadcast it in your local organization and in your "normal contacts".

To avoid duplications I'm sendig also (at the end) a list (organized by Walther Neuper) 

showing some of the broadcasting addresses used already fot the 1st call for papers for THedu'12.

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

2nd CALL FOR PAPERS

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

THedu'12

TP components for educational software

11 July 2012

http://www.uc.pt/en/congressos/thedu/thedu12

Workshop at CICM 2012

Conferences on Intelligent Computer Mathematics

9-14 July 2012

Jacobs University, Bremen, Germany

http://www.informatik.uni-bremen.de/cicm2012/cicm.php

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

THedu'12 Scope

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

This workshop intends 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 workshop tries to combine and

focus systems of these areas 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 involve 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 Euclidian 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 inquiry-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. However, 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, TP 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, use the methods' knowledge to generate user-guidance

mechanically, this 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 series 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 Committee

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

Ralph-Johan Back, Abo Akademy University, Finland

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

Filip Maric, University of Belgrade, Serbia

Walther Neuper, Graz University of Technology, Austria

Pedro Quaresma, University of Coimbra, Portugal

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

Important Dates (by easychair)

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

* 01 May 2012 * Extended Abstracts/Demo proposals

* 01 Jun 2012 * Author Notification

* 15 Jun 2012 * Final Version

* 11 Jul 2012 * Worshop Day

* 31 Aug 2012 * Full papers (EPTCS post-proceedings)

Submission

----------

We welcome submission of proposals to present a demo, as well as

submissions of extended abstracts (5-8 pages max) presenting original

unpublished work which is not been submitted for publication

elsewhere.

Selected extended abstracts will appear in CISUC Technical Report

series (ISSN 0874-338X [1]). All accepted extended abstracts and

system demos will be presented at the workshop, and the extended

abstracts will be made available online.

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

easychair [2].

Extended abstracts should be 5-8 pages in length and are to be

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

guidelines [3].

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

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

abstract/demo.

The post-proceedings (full papers, 20 pages max) will be published in

the Electronic Proceedings in Theoretical Computer Science (EPTCS)

series [4].

---

[1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/

[2] http://www.easychair.org/conferences/?conf=thedu12

[3] http://http://style.eptcs.org/

[4] http://eptcs.org/

============================================

THedu addresses for CfP

120227

###########################################################################

Pedro   --> Francisco, Julien, Marvin, Laurent

Walther --> Cezary, Makarius, Judit, Csaba

###########################################################################

acl2@utlists.utexas.edu;;Walther Neuper;;  ;c1;; ;c2;; ;c3;			;   SUBSCRIBED	;   	;  

//aisb@cogs.sussex.ac.uk;   list abandoned;   Centre.Resear.Cog.Sci			;   	;  

//announce@sigart.acm.org;  list abandoned;   ACM Spec.Int.Group AI			;   

cade@itu.dk;;;;;Pedro Quaresma  	;   ;c1;; ;c2;; ;c3;

						;   	;  

coq-club@pauillac.inria.fr; Julien Narboux;;  ;c1;; ;c2;; ;c3;

						;   	;  

//DAI-List-Request@ece.sc.edu  list abandoned;   univ.south carolina, CS			;   	;  

//event@in.tu-clausthal.de; list abandoned

						;   	;  

CCSA 2011 (and SCDG);;   Francisco Botana;;;c1;; ;c2;; ;c3;

						;   	;  

hol-info@lists.sourceforge.net Cezary Kaliszyk;; ;c1;; ;c2;; ;c3;

isabelle-users@cl.cam.ac.uk;Makarius Wenzel;; ;c1;; ;c2;; ;c3;

						;   	;  

//isabelle-dev@in.tum.de;   Alex Kraus: NOT for CfPs!

						;   	;  

kr@kr.org;;;;;  Walther Neuper  	;   ;c1;; ;c2;; ;c3;;   list: Knowledge Representation and Reasoning;	;  

lics@informatik.hu-berlin.de   Walther Neuper	;   ;c1;; ;c2;; ;c3;

limbaje@cs.ubbcluj.ro	;   Judit Robu	;   ;c1;; ;c2;; ;c3;

logic@math.uni-bonn.de	;   Marvin Schiller;; ;c1;; ;c2;; ;c3;

MATHEDU@JISCMAIL.AC.UK;; Pedro Quaresma (J.Silva);c1;; ;c2;; ;c3;

						;   	;  

metaprl-users@metaprl.org;  Walther Neuper;;  ;c1;; ;c2;; ;c3;

mizar-forum@mizar.uwb.edu.pl   Makarius		;   ;c1;; ;c2;; ;c3;

						;   	;  

//om-announce@openmath.org; replaced b.MathWeb

						;   	;  

poplmark@lists.seas.upenn.edu  Walther Neuper;;  ;c1;; ;c2;; ;c3;

project-calculemus@lists.jacobs-university.de	;   ;c1;; ;c2;; ;c3;

			;   Laurent Théry	;  

projects-mkm-ig@jacobs-university.de;;;;   ;c1;; ;c2;; ;c3;

			;   Walther Neuper SUBSCRIBED

project-MathWeb-announce@jacobs-university.de	;   ;c1;; ;c2;; ;c3;

;;;;;;;   Walther Neuper SUBSCRIBED;;

proofpower@lemma-one.com;   Walther Neuper;;  ;c1;; ;c2;; ;c3;

pvs@csl.sri.com;;;;Makarius		;   ;c1;; ;c2;; ;c3;

						;   	;  

rewriting@ens-lyon.fr;;  Pedro Quaresma;;  ;c1;; ;c2;; ;c3;

;   needs to be SUBSCRIBED

sem@fc.ul.pt;;;;   Pedro Quaresma (J.Silva);c1;; ;c2;; ;c3;

						;   	;  

sisteme@cs.ubbcluj.ro	;   Judit Robu	;   ;c1;; ;c2;; ;c3;

TecMat@yahoogrupos.com.br;  Pedro Quaresma (J.Silva);c1;; ;c2;; ;c3;

						;   	;  

theorem-provers@ai.mit.edu; Walther Neuper;;  ;c1;; ;c2;; ;c3;			;   SUBSCRIBED	;   	;  

theory-logic@CS.CMU.EDU;;Pedro Quaresma;;  ;c1;; ;c2;; ;c3;

//twelf-list@twelf.org;; 2011: "User unkown"

types-announce@lists.seas.upenn.edu;;;;;;c1;; ;c2;; ;c3;

;;;;;;;   Cezary Kaliszyk;;  

types@lists.chalmers.se;;Cezary Kaliszyk;; ;c1;; ;c2;; ;c3;

vki-list@dfki.de;;;   Pedro Quaresma  	;   ;c1;; ;c2;; ;c3;;   Ges.f.Inf - Spec.Int.Group on DAI	;   	;  

webmath@camel.math.ca;;  Pedro Quaresma (J.Silva);c1;; ;c2;; ;c3;

							;  

zzz.hu			;   Csaba Sárvári	;   ;c1;; ;c2;; ;c3;

--

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