[isabelle] last CfP ThEdu'14 at CICM Coimbra

               Last Call for Extended Abstracts & Demonstrations
                    TP components for educational software
                                Wed.9. July 2014

                                  at CICM 2014
                  Conferences on Intelligent Computer Mathematics
                          University Coimbra, Portugal
                                co-located with
                                   ADG 2014
        10th International Workshop on Automated Deduction in Geometry
                           University of Coimbra, Portugal

THedu'14 Scope

THedu is a forum 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 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.

Important Dates

     * Extended Abstracts:     25 May 2014
     * Author Notification:    08 June 2014
     * Final Version:          22 June 2014
     * Workshop Day:           09 July 2014


ThEdu's aims
address elements for next-generation assistants, which 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
  post-conditions 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 specialised 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 Step-wise 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, using the methods' knowledge to generate user-guidance
  mechanically is an appealing challenge for ATP and ITP, and probably
  for compiler construction.

  * Pedagogical strategies: Using TP technologies in learning
  environments call for strategies for linking and adapting the
  availble tools for specific educational needs and new methods for
  the management of mathematical knowledge capable of filling the gap
  between repositories and end-user system and new visual and/or
  natural language interfaces to allow the use of rigorous reasoning
  methods and tools.

  In principle, mathematical software can be conceived as models of
  mathematics: The challenge addressed by this workshop is to provide
  appealing models for mathematics assistants which are interactive
  and which explain themselves such that interested students can
  independently learn by inquiry and experimentation.


We welcome submission of extended abstracts and demonstration
proposals presenting original unpublished work which is not been
submitted for publication elsewhere.

All accepted extended abstracts and demonstrations will be presented
at the workshop. The extended abstracts will be made available

Extended abstracts and demonstration proposals should be submitted via
THedu'14 easychair (https://www.easychair.org/conferences/?conf=thedu14).

Extended abstracts and demonstration proposals should be no more than
4 pages in length and are to be submitted in PDF format. They must
conform to the EPTCS style guidelines (http://style.eptcs.org/).

At least one author of each accepted extended abstract/demonstration
proposal is expected to attend THedu'14 and presents his/her extended

Program Committee
    Francisco Botana, University of Vigo at Pontevedra, Spain
    Roman Hasek, University of South Bohemia, Czech Republic
    Filip Maric, University of Belgrade, Serbia
    Walther Neuper, Graz University of Technology, Austria (co-chair)
    Pedro Quaresma, University of Coimbra, Portugal (co-chair)
    Vanda Santos, CISUC, Portugal
    Wolfgang Schreiner, Johannes Kepler University, Austria

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.