[Thedu] THedu12 at CICM 2012
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