*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Last CfP "Justifying (in) Math" at CADGME 2016*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Sat, 23 Apr 2016 15:43:35 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Final Call for Abstracts and Posters - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - eduTPS: "Justifying (in) Math" Working Group on Education and TP Technology - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - at CADGME 2016 September 7-10, 2016, Targu Mures, Romania https://cadgme.ms.sapientia.ro/ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - New Deadline: Abstracts: May 2, 2016 Posters: May 2, 2016 The abstracts of contributed talks and posters will be published on the conference proceedings website. The length is maximum 300 words. Abstracts and posters should be submitted in as unformatted texts on the Easy Chair system: https://easychair.org/conferences/?conf=cadgme2016 Aims of the working group eduTPS: Mathematics is not only calculating, numeric and symbolic calculation, not only explaining with figures --- the distiguishing feature of math is justifying and deducing properties of mathematical objects and operations on firm grounds of logics. So Computer Algebra Systems (CAS) model calculation, Dynamic Geometry Systems (DGS) model figures --- and (Computer) Theorem Provers (TPS) model deduction and reasoning, mechanised by formal logic. TPS are widely unknown despite the fact, that recent advances in mathematics could not have been done without them (e.g. mechanised proofs of the Four Colour Theorem, of the Kepler Conjecture, etc.), that TPS are becoming indispensable in verification of requirements on complex technical systems (e.g. google car) and despite the fact, that leading TPS have math mechanised from first principles (axioms) to all undergraduate math and beyond. So the working group "eduTPS: justifying math" addresses a wide range of topics, from educational concepts of reasoning, explaining and justifying and from respective classroom experience on the one side to technical concepts and software tools, which mechanise and support these mathematical activities, on the other side. We elicit contributions from educators to the educational side as well as TP experts to the technical side --- the working group shall interactively elaborate on the connections between the two sides, connections which are not yet clarified to a considerable extent. Narrowing the apparent gap between TP technology and educational practice (and theory!) concerns the distinguishing essence of mathematics and may well lead to considerable innovations in how we teach and learn mathematics in the future. Points of interest include: * Adaption of TP -- concepts and technologies for education: knowledge representation, simplifiers, reasoners; undefinednes, level of abstraction, etc. * Requirements on software support for reasoning -- reasoning appears as the most advanced method of human thought, so at which age which kind of support by TP should be provided? * Automated TP in geometry -- relating intuitive evidence with logical rigor: specific provers, adaption of axioms and theorems, visual proofs, etc. * TP components in SW for engineers -- Formal Methods increasingly advance into engineering practice, so educational software based on TP components could anticipate that advancement. * Levels of authoring -- in order to cope with generality of TP: experts adapt to specifics of countries or levels, teachers adapt to courses and students. * Adaptive dialogues, students modeling and learning paths -- services for user guidance provided by TP technology: which interfaces enable flexible generation of adaptive user guidance? * Next-step-guidance -- suggesting a next step when a student gets stuck in problem solving: which computational methods can extend TP for that purpose? * TP as unifying foundation -- for the integration of technologies like CAS, DGS, Spreadsheets etc: interfaces for unified support of reasoning? * Continuous tool chains -- for mathematics education from high-school to university, from algebra and geometry to graph theory, from educational tools to professional tools for engineers and scientists. Programme Committee: Roman HaÅek, University of South Bohemia, Czech Republic ZoltÃn KovÃcs, Johannes Kepler University, Austria Filip Maric, University of Belgrade, Serbia Walther Neuper, Graz University of Technology, Austria (co-chair) Pavel Pech, University of South Bohemia, Czech Republic Pedro Quaresma, University of Coimbra, Portugal (co-chair) Judit Robu, BabeÅ-Bolyai University Cluj, Romania Vanda Santos, CISUC, Portugal RÃbert Vajda, University of Szeged, Hungary Wolfgang Windsteiger, Johannes Kepler University, Austria

- Previous by Date: Re: [isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering
- Next by Date: [isabelle] Type variables, locale import and notation
- Previous by Thread: [isabelle] HOFM @ STAF / SEFM 2016: call for papers
- Next by Thread: [isabelle] Type variables, locale import and notation
- Cl-isabelle-users April 2016 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