[Thedu] THedu12 1st call for papers

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

Dear THeduers

In attachment the THedu'12 1st call for papers, Please broadcast it in your 
local organization and your "normal contacts".

To avoid duplications I'm sendig also a file (organized by Walther Neuper) 
showing some of the broadcasting addresses used for THedu'11.

-- 
  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

----------------------------------------------------------------------
                              CALL FOR PAPERS
----------------------------------------------------------------------
                                 THedu'12
                   TP components for educational software
                                11 July 2012
                    http://www.uc.pt/en/congressos/thedu

                            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 Euklidian 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 University, Turku, 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)
---------------

    * Extended Abstracts/Demo proposals:  01 May 2012
    * Author Notification:                01 Jun 2012
    * Final Version:                      15 Jun 2012
    * Worshop Day:                        11 Jul 2012


Submission
----------

We welcome submission of proposals to present a demo, as well as
submissions of extended abstracts (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. A publication
post-proceedings (papers, 15 pages max) under EPTCS is under
consideration.

Extended abstracts and demo proposals should be submitted via THedu'12
easychair [2].

Extended abstracts should be no more than 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.

[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/

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;