×

Flexary connectives in Mizar. (English) Zbl 1387.68207

Summary: One of the main components of the Mizar project is the Mizar language, a computer language invented to reflect the natural language of mathematics. From the very beginning various linguistic constructions and grammar rules which enable us to write texts which resemble classical mathematical papers have been developed and implemented in the language. The Mizar Mathematical Library is a repository of computer-verified mathematical texts written in the Mizar language. Besides well-known and important theorems, the library contains series of some quite technical lemmas describing some properties formulated for different values of numbers. For example the sequence of lemmas \[ \begin{aligned} &\mathtt{for\;\; n\;\; being\;\; Nat\;\; st\;\; n\;\; <=\; 1\;\; holds \;\; n=0\;\; or \;\; n=1;}\\ &\mathtt{for\;\; n\;\; being\;\; Nat\;\; st\;\; n\;\; <=\; 2\;\; holds \;\; n=0\;\; or \;\; n=1\;\; or\;\; n=2;}\\ &\mathtt{for\;\; n\;\; being\;\; Nat\;\; st\;\; n\;\; <=\; 3\;\; holds \;\; n=0\;\; or \;\; n=1\;\; or\;\; n=2\;\; or\;\; n=3;} \end{aligned} \] which for a long time contained 13 such formulae. In this paper, we present an extension of the Mizar language – an ellipsis that is used to define flexary logical connectives. We define flexary conjunction and flexary disjunction, which can be understood as generalization of classical conjunction and classical disjunction, respectively. The proposed extension enables us to get rid of lists of such lemmas and to formulate them as single theorems, e.g., \[ \mathtt{for} \;\; \mathtt{m,}\;\; \mathtt{n}\;\; \mathtt{being}\;\; \mathtt{Nat}\;\; \mathtt{st}\;\; \mathtt{n}\;\; \mathtt{<=}\;\; \mathtt{m}\;\; \mathtt{holds\;\; n=0 \;\;or \dots or\;\; n=m;} \] covering all cases between the bounds 0 and m in this case. Moreover, a specific inference rule to process flexary formulae, formulae using flexary connectives, is introduced. We describe how ellipses are incorporated into the Mizar language and how they are verified by the Mizar proof checker.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI

References:

[6] Bancerek, G., On the structure of Mizar types, (Geuvers, H.; Kamareddine, F., Electronic notes in theoretical computer science, 85 (2003), Elsevier B.V.), 69-85 · Zbl 1264.03040
[8] Bancerek, G.; Rudnicki, P., A compendium of continuous lattices in Mizarformalizing recent mathematics, J Autom Reason, 29, 3-4, 189-224 (2002) · Zbl 1064.68082
[11] Caminati, M. B.; Korniłowicz, A., Pseudo-canonical formulae are classical, Formaliz Math, 22, 2, 99-103 (2014), 〈http://dx.doi.org/10.2478/forma-2014-0011〉 · Zbl 1352.03013
[15] Fitch, F. B., Symbolic logic, an introduction (1952), Ronald Press Co: Ronald Press Co New York · Zbl 0049.00504
[17] Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M. W.; Scott, D. S., A compendium of continuous lattices (1980), Springer-Verlag: Springer-Verlag Berlin, Heidelberg, New York · Zbl 0452.06001
[22] Grabowski, A.; Kornilowicz, A.; Naumowicz, A., Mizar in a nutshell, J Formaliz Reason Special IssueUser Tutor I, 3, 2, 153-245 (2010) · Zbl 1211.68369
[42] Okazaki, H.; Shidama, Y., Formalization of the data encryption standard, Formaliz Math, 20, 2, 125-146 (2012), 〈http://dx.doi.org/10.2478/v10037-012-0016-y〉 · Zbl 1288.94079
[43] Ono, K., On a practical way of describing formal deductions, Nagoya Math J, 21, 115-121 (1962) · Zbl 0111.00703
[46] Rudnicki, P., Obvious inferences, J Autom Reason, 3, 4, 383-393 (1987) · Zbl 0641.68141
[48] Schwarzweller, C., Proth numbers, Formaliz Math, 22, 2, 111-118 (2014), 〈http://dx.doi.org/10.2478/forma-2014-0013〉 · Zbl 1352.11010
[49] Sexton, A. P.; Sorge, V., Abstract matrices in symbolic computation, (Dumas, J.-G., International symposium on symbolic and algebraic computation (ISSAC) (July 2006), ACM Press: ACM Press Genova, Italy), 318-325 · Zbl 1356.68294
[51] Tarski, A., On well-ordered subsets of any set, Fundam Math, 32, 176-183 (1939) · JFM 65.1165.01
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.