A path to faithful formalizations of mathematics

G.I. Jojgov; R.P. Nederpelt

doi:10.1007/978-3-540-27818-4_11

A path to faithful formalizations of mathematics

G.I. Jojgov, R.P. Nederpelt

Model Driven Software Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

Abstract

In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we can have a fairly high confidence that we have produced a ‘faithful’ formalization (i.e. that the formal text is as close as possible to the intentions expressed in the informal text). A computer program that assists a human along the formalization path should create enough "added value" to be useful in practice. We also discuss some problems that such an implementation needs to solve and possible solutions for them.

Original language	English
Title of host publication	Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004)
Editors	A. Asperti, G. Bancerek, A. Trybulec
Place of Publication	Berlin
Publisher	Springer
Pages	145-159
ISBN (Print)	3-540-23029-7
DOIs	https://doi.org/10.1007/978-3-540-27818-4_11
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	3119
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-540-27818-4_11

Fingerprint Dive into the research topics of 'A path to faithful formalizations of mathematics'. Together they form a unique fingerprint.

Cite this

Jojgov, G. I., & Nederpelt, R. P. (2004). A path to faithful formalizations of mathematics. In A. Asperti, G. Bancerek, & A. Trybulec (Eds.), Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004) (pp. 145-159). (Lecture Notes in Computer Science; Vol. 3119). Berlin: Springer. https://doi.org/10.1007/978-3-540-27818-4_11

@inproceedings{0ab25cca6c1f40e0b8fb542583d846cf,

title = "A path to faithful formalizations of mathematics",

abstract = "In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we can have a fairly high confidence that we have produced a ‘faithful’ formalization (i.e. that the formal text is as close as possible to the intentions expressed in the informal text). A computer program that assists a human along the formalization path should create enough {"}added value{"} to be useful in practice. We also discuss some problems that such an implementation needs to solve and possible solutions for them.",

author = "G.I. Jojgov and R.P. Nederpelt",

year = "2004",

doi = "10.1007/978-3-540-27818-4_11",

language = "English",

isbn = "3-540-23029-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "145--159",

editor = "A. Asperti and G. Bancerek and A. Trybulec",

booktitle = "Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004)",

address = "Germany",

}

Jojgov, GI & Nederpelt, RP 2004, A path to faithful formalizations of mathematics. in A Asperti, G Bancerek & A Trybulec (eds), Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004). Lecture Notes in Computer Science, vol. 3119, Springer, Berlin, pp. 145-159. https://doi.org/10.1007/978-3-540-27818-4_11

A path to faithful formalizations of mathematics. / Jojgov, G.I.; Nederpelt, R.P.

Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004). ed. / A. Asperti; G. Bancerek; A. Trybulec. Berlin : Springer, 2004. p. 145-159 (Lecture Notes in Computer Science; Vol. 3119).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A path to faithful formalizations of mathematics

AU - Jojgov, G.I.

AU - Nederpelt, R.P.

PY - 2004

Y1 - 2004

N2 - In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we can have a fairly high confidence that we have produced a ‘faithful’ formalization (i.e. that the formal text is as close as possible to the intentions expressed in the informal text). A computer program that assists a human along the formalization path should create enough "added value" to be useful in practice. We also discuss some problems that such an implementation needs to solve and possible solutions for them.

AB - In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we can have a fairly high confidence that we have produced a ‘faithful’ formalization (i.e. that the formal text is as close as possible to the intentions expressed in the informal text). A computer program that assists a human along the formalization path should create enough "added value" to be useful in practice. We also discuss some problems that such an implementation needs to solve and possible solutions for them.

U2 - 10.1007/978-3-540-27818-4_11

DO - 10.1007/978-3-540-27818-4_11

M3 - Conference contribution

SN - 3-540-23029-7

T3 - Lecture Notes in Computer Science

SP - 145

EP - 159

BT - Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004)

A2 - Asperti, A.

A2 - Bancerek, G.

A2 - Trybulec, A.

PB - Springer

CY - Berlin

ER -

Jojgov GI, Nederpelt RP. A path to faithful formalizations of mathematics. In Asperti A, Bancerek G, Trybulec A, editors, Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004). Berlin: Springer. 2004. p. 145-159. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-27818-4_11