Equality in computer proof-assistants
Adam Grabowski, Artur Kornilowicz, Christoph Schwarzweller
DOI: http://dx.doi.org/10.15439/2015F229
Citation: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 5, pages 45–54 (2015)
Abstract. Equality is fundamental notion of logic and mathematics as a whole. If computer-supported formalization of knowledge is taken into account, sooner or later one should precisely declare the intended meaning/interpretation of the primitive predicate symbol of equality. In the paper we draw some issues how computerized proof-assistants can deal with this notion, and at the same time, we propose solutions, which are not contradictory with mathematical tradition and readability of the source code. Our discussion is illustrated with examples taken from the implementation of the Mizar system.