# [isabelle] 2nd CfP: THedu'11 at CADE

[Apologies for possible multiple postings.]
----------------------------------------------------------------------
CALL FOR PAPERS
----------------------------------------------------------------------
THedu'11
CTP components for educational software
=======================================
(CTP -- Computer Theorem Proving)
http://www.uc.pt/en/congressos/thedu
Workshop at CADE-23,
23nd International Conference on Automated Deduction
Wroclaw, Poland, July 31- August 5, 2011
http://cade23.ii.uni.wroc.pl/
----------------------------------------------------------------------
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 Haftman, 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
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])
Submission
----------

`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].
`
[1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/
[2] http://www.easychair.org/conferences/?conf=thedu11
[3] http://www.cse.unsw.edu.au/%7Ervg/EPTCS/eptcsstyle.zip

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