*To*: "isabelle-users at cl.cam.ac.uk >> isabelle-users" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] last CfP ThEdu'14 at CICM Coimbra*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Mon, 19 May 2014 13:33:22 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

---------------------------------------------------------------------- Last Call for Extended Abstracts & Demonstrations ---------------------------------------------------------------------- ThEdu'14 TP components for educational software Wed.9. July 2014 (http://www.uc.pt/en/congressos/thedu/thedu14) at CICM 2014 Conferences on Intelligent Computer Mathematics University Coimbra, Portugal http://cicm-conference.org/2014/cicm.php co-located with ADG 2014 10th International Workshop on Automated Deduction in Geometry University of Coimbra, Portugal http://www.uc.pt/en/congressos/adg/adg2014/ ---------------------------------------------------------------------- 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 (https://www.easychair.org/conferences/?conf=thedu14) 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. Submission ---------- 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 online. 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 abstract/demonstration. 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 --------------------------------------------------------------------

- Previous by Date: Re: [isabelle] Isar parser for constant names
- Next by Date: Re: [isabelle] Isar parser for constant names
- Previous by Thread: Re: [isabelle] quickchecking lemma with types defined by typedecl
- Next by Thread: [isabelle] ISR 2014: call for participation
- Cl-isabelle-users May 2014 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