Lista thedu

Mensagem

[Thedu] THedu12 at CICM 2012

To :   thedu@uc.pt
Subject :   [Thedu] THedu12 at CICM 2012
From :   Pedro Quaresma <pedro@mat.uc.pt>
Date :   Mon, 16 Jan 2012 10:08:05 +0000

Em Domingo, 15 de Janeiro de 2012, escreveu:
> Dear Pedro,
> 
> I am sorry for the long silence, ...
> 

Dear THeduers

Good news, our workshop, THedu'12, as just been accepted in CICM 2012.

> we are happy to accept your workshop at CICM 2012. Here is our current
> thinking about the organization and finances
> 

let's begin working on that (I already discussed with my PhD student some 
ideas about a possible submission).

Pedro Quaresma

> Workshops will be on Wed July 11 and Sat July 14. We suggest Wed for THedu.
> 
> WS participants have to register at CICM through the regular interface.
> Conference participants register for an additional day, "WS only"
> participants for the workshop only (current estimation 50/25 Euro for
> regular/students for both).
> 
> CICM provides a room, printed workshop proceedings (deadline tbd), joint
> coffee breaks, lunch, and a space on the CICM web pages.
> 
> We will keep you updated, please feel free to ask if something is unclear.
> 
> Michael & Serge
> 
> On 18.11.11 16:41, Pedro Quaresma wrote:
> > Dear Michael Kohlhase
> > 
> > The following text is our submission of THedu'12 as a workshop of CICM
> > 2012.
> > 
> > Hopping for a good outcome, yours sincerely.
> > 
> > Pedro Quaresma
> > 
> > 
> > <thedu12proposal>
> > 
> > CICM 2012 - Conference on Intelligent Computer Mathematics
> > July 9-13, 2012 at Jacobs University, Bremen, Germany
> > 
> > Workshop Proposal
> > 
> > Workshop title:
> >    THedu'12 - CTP Components for Educational Software
> > 
> > Names and affiliations of organizers:
> >    Chairs
> >    
> >     Ralph-Johan Back, Abo University, Turku, Finland
> >     Pedro Quaresma, University of Coimbra, Portugal
> >    
> >    Program Committee
> >    
> >     Ralf-Johan Back,  Abo University, Turku, Finland
> >     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
> >     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
> > 
> > Brief description of workshop goals and/or topics:
> >    The THedu group 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 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 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 enquiry-based learning from concrete to
> >      abstract --- and the knowledge's logical coherence supports such
> >      learning: for instance, the formula 2.π 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 tracable 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, use 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.
> > 
> > Proposed workshop duration:
> >    1 day
> > 
> > Conference affiliation for the previous meeting:
> >    THedu'11 was associated to CADE23
> >    (http://www.uc.pt/en/congressos/thedu/thedu11/)
> > 
> > Informal proceedings:
> >    Following THedu'11 practise we expect to have a abstracts only
> >    informal proceedings to be available during the workshop and we intend
> >    to apply to Electronic Proceedings in Theoretical Computer Science
> >    (EPTCS) to the post-conference proceedings (the THedu'11
> >    post-proceedings will be published by EPTCS).
> > 
> > </thedu12proposal>


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

Mensagem anterior por data: Re: [Thedu] THedu'12 - submission of a workshop proposal Próxima mensagem por data: Re: [Thedu] EPTCS: THedu'11 Proceedings
Mensagem anterior por assunto: [Thedu] THedu'12 at AAR Newsletter No. 97 Próxima mensagem por assunto: [Thedu] THedu'12 poster and 1st call for papers