27-31 Jul 2020
Announcement and Call for Papers Workshop on Natural Formal Mathematics (NFM 2020) A workshop held between July 27 - 31, 2020 as part of the 13th Conference on Intelligent Computer Mathematics (CICM 2020) (ONLINE; details to be announced on the CICM website https://cicm-conference.org/2020/cicm.php) In (pure) mathematics there has always existed a strong informal sense of "naturality". "Natural" theories, notions, properties, or proofs are prefered over technical, convoluted, or counterintuitive approaches. If formal mathematics is to become part of mainstream mathematics, its formalizations and user experience have to become more "natural". This workshop broadly addresses the issue of naturality in formal mathematics. Topics of interest include (but are not limited to): The notion of naturality in mathematics generally Natural input and output languages for formal mathematics systems Parsing natural mathematical language Controlled natural languages (CNL) for mathematics Making formal mathematics documents readable Naturality of foundational theories (types, sets, HOL, ...) Naturality of proof methods Natural proof structures and granularities Natural structurings of formalized mathematical texts and libraries Mathematical type setting (LaTeX) and formal mathematics Examples of natural formalizations Invited speaker: tba Submissions: We call for submissions of extended abstracts and demonstration proposals presenting work related to the workshop's topics of interest. To promote Natural Formal Mathematics unfinished or exploratory work will also be welcome. Electronic submission is done through EasyChair. Extended abstracts and demonstration proposals should be 1 page, formatted in LaTeX using the style onecolceurws. Submission deadline: June 15 2020 Notification of acceptance: July 01 2020 Accepted papers and demonstrations should be presented online and live, to allow for questions and discussions. Abstracts will be made available online. Program Committee Florian Rabe, Erlangen (co-chair) Peter Koepke, Bonn (co-chair) Merlin Carl, Flensburg Marcos Cramer, Dresden Adam Grabowski, Bialystok Michael Junk, Konstanz Cezary Kaliszyk, Innsbruck Andrea Kohlhase, Neu-Ulm Aarne Ranta, Gothenburg Josef Urban, Prague -- [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