*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] THedu12 1st call for papers*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Mon, 27 Feb 2012 16:23:52 +0100*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.26) Gecko/20120131 Thunderbird/3.1.18

With apologies for multiple postings ! ---------------------------------------------------------------------- CALL FOR PAPERS ---------------------------------------------------------------------- THedu'12 TP components for educational software 11 July 2012 http://www.uc.pt/en/congressos/thedu Workshop at CICM 2012 Conferences on Intelligent Computer Mathematics 9-14. July 2012 Jacobs University, Bremen, Germany http://www.informatik.uni-bremen.de/cicm2012/cicm.php ---------------------------------------------------------------------- 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 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 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 University, Turku, 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) --------------- * Extended Abstracts/Demo proposals: 01 May 2012 * Author Notification: 01 Jun 2012 * Final Version: 15 Jun 2012 * Worshop Day: 11 Jul 2012 Submission ---------- We welcome submission of proposals to present a demo, as well as submissions of extended abstracts (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 online. A publication post-proceedings (papers, 15 pages max) under EPTCS is under consideration. Extended abstracts and demo proposals should be submitted via THedu'12 easychair [2]. Extended abstracts should be no more than 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. [1]http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/ [2]http://www.easychair.org/conferences/?conf=thedu12 [3]http://http://style.eptcs.org/

- Previous by Date: Re: [isabelle] Syntax, translations inside a locale
- Next by Date: [isabelle] CfP: IJCAR Workshop on Automated Theory Exploration
- Previous by Thread: [isabelle] Call for Journal Papers: STVR Special Issue on Tests and Proofs
- Next by Thread: [isabelle] CfP: IJCAR Workshop on Automated Theory Exploration
- Cl-isabelle-users February 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list