The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » Education » mathedu

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: THedu'12 - 2nd call for papers
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List

Posts: 23
Registered: 5/3/06
THedu'12 - 2nd call for papers
Posted: Apr 17, 2012 5:33 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

[Apologies if you receive multiple copies]

TP components for educational software
11 July 2012

Workshop at CICM 2012
Conferences on Intelligent Computer Mathematics
9-14 July 2012
Jacobs University, Bremen, Germany


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

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


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

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

[3] http://

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
telef: +351 239 791 137; fax: +351 239 832 568

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.