25-29 Jul 2016
Bialystock, Poland
======================================================================= Call for Extended Abstracts & Demonstrations - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ThEdu'16 Theorem Prover Components for Educational Software http://www.uc.pt/en/congressos/thedu/thedu16 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - at CICM 2016 Conferences on Intelligent Computer Mathematics July 25-29, 2016, Bialystok, Poland http://www.cicm-conference.org/2016 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - THedu'16 Scope: Educational software tools have technologies integrated from CAS, from DGS, from Spreadsheets and others, but not from (Computer) Theorem Provers (TPs) with few exceptions: the latter have been developed to model mathematical reasoning in software -- rigorous reasoning as a companion of calculating, which guarantees the unsurpassed reliability of mathematics. Providing students with insight in and experience with this kind of reliability is considered an essential aim of mathematics education. TPs intrude into science as well as into industry: They are used to tackle difficult proofs in the science of mathematics, like the Four Color Theorem or the Kepler Conjecture. In industry TPs are successfully used to verify safety critical software. This workshop addresses a window of opportunity during the still open development of TPs. The workshop provides a meeting place for educators and developers of educational mathematics software and experts in TP. The discussions shall clarify the requirements of education, identify advantages and promises of TP for learning and motivate development of such a novel kind of educational mathematical tools. Important Dates * Extended Abstracts: 4. June 2016 * Author Notification: 18. June 2016 * Final Version: 2. July 2016 * Workshop Day: 25-29. July 2016 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 TP should be provided? * Automated TP in geometry -- relating intuitive evidence with logical rigor: specific provers, adaption of axioms and theorems, visual proofs, etc. * Application of 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 modules, 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 etc. 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. Contributions should be submitted via THedu'16 easychair https://www.easychair.org/conferences/?conf=thedu16. 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'15 and presents his/her extended abstract/demonstration. Joint publication in companion with other CICM events is under consideration (e.g. http://ceur-ws.org/). Program Committee Francisco Botana, University of Vigo at Pontevedra, Spain Roman Ha?ek, University of South Bohemia, Czech Republic Filip Maric, University of Belgrade, Serbia Walther Neuper, TUG University of Technology, Austria (co-chair) Pavel Pech, University of South Bohemia, Czech Republic Pedro Quaresma, University of Coimbra, Portugal (co-chair) Vanda Santos, CISUC, Portugal Wolfgang Schreiner, Johannes Kepler University, Austria Burkhart Wolff, University Paris-Sud, France -- [LOGIC] mailing list http://www.dvmlg.de/mailingliste.html Archive: http://www.illc.uva.nl/LogicList/ provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam