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'11 at CADE: last call for ext.abstracts
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List

Posts: 23
Registered: 5/3/06
THedu'11 at CADE: last call for ext.abstracts
Posted: Apr 21, 2011 7:33 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

CTP components for educational software
(CTP -- Computer Theorem Proving)

Workshop at CADE-23,
23nd International Conference on Automated Deduction
Wroclaw, Poland, July 31- August 5, 2011
Important Dates
* Extended Abstracts/Demo proposals 29 Apr 2011 (PDF, easychair [2])
* Author Notification: 3 Jun 2011
* Worshop Day: 31 Jul 2011
* Full papers (post-proceedings): 27 Aug 2011 (LaTeX,easychair[2])

THedu'11 Scope
This workshop 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
and 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 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 Euclidean 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.pi depends on the
definition of reals and of multiplication; close to these definitions
are the laws like commutativity etc. Clearly, 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, 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, using 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.

Program Chairs
Ralph-Johan Back, Abo University, Turku, Finland
Pedro Quaresma, University of Coimbra, Portugal

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

THedu'11 seeks papers and demos presenting original unpublished work
which is not been submitted for publication elsewhere.

Both, papers and demos, are submitted as extended abstracts first (29
Apr 2011), which must not exceed five pages. The abstract should be new
material. Demos should be accompanied by links to demos/downloads and
[existing] system descriptions. Availability of such accompanying
material will be a strong prerequisite for acceptance.

The authors of the extended abstracts and system descriptions should
submit to easychair [2] in PDF format generated by EPTCS LaTeX style [3]
. Selected extended abstracts and system descriptions will appear in
CISUC Technical Report series (ISSN 0874-338X, [1]).

At least one author of each accepted paper/demo is expected to attend
THedu'11 and to present her or his paper/demo, and the extended
abstracts will be made available online.

After presentation at the conference selected authors will be invited to
submit a substantially revised version, extended to 10-14 pages, for
publication by the Electronic Proceedings in Theoretical Computer
Science (EPTCS). Papers/system descriptions will be reviewed by blind
peer review and evaluated by three referees with respect to relevance,
clarity, quality, originality, and impact.

Revised versions are submitted in LaTeX according to the EPTCS style
guidelines [3] via easychair [2].


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