<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

A Survey of Languages for Formalizing Mathematics

descriptionPublicationkeyboard_double_arrow_right Part of book or chapter of book , Article , Preprint , Conference object , Other literature type 01 Jan 2020Embargo end date: 01 Jan 2020 Austria English Publisher:Springer International PublishingFunded by:EC | OpenDreamKit, EC | SMART

Authors: Cezary Kaliszyk; Florian Rabe;

doi: 10.1007/978-3-030-53518-6_9 , 10.48550/arxiv.2005.12876

arXiv: http://arxiv.org/abs/2005.12876

A Survey of Languages for Formalizing Mathematics

- Summary
- Subjects
- Metrics

Abstract

In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce human-readable documents. These goals are challenging to combine and state-of-the-art tools typically have to make difficult compromises. In this paper we discuss languages that have been created for this purpose, including logical languages of proof assistants and other formal systems, semi-formal languages, intermediate languages for exchanging mathematical knowledge, and language frameworks that allow building customized languages. We evaluate their advantages based on our experience in designing and applying languages and tools for formalizing mathematics. We reach the conclusion that no existing language is truly good enough yet and derive ideas for possible future improvements.

CICM 2020 conference paper preprint

Country

Austria

Related Organizations

University of Erlangen-Nuremberg
Germany
University of Innsbruck
Austria

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in Computer Science (cs.LO)

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	7
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Top 10%
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Top 10%