Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The Mizar system [1–3] is a computer system invented for computer-assisted verification of mathematical papers. It consists of three main components: a language – the Mizar language, a bunch of computer programs including Verifier and a repository of formal texts – Mizar Mathematical Library (MML) – written in the language and automatically verified for their logical correctness. The Mizar language is a declarative formal language designed to write mathematical papers readable for humans and effectively processed by computers. The language is highly structured to ensure producing rigorous and semantically unambiguous texts. Apart from rules for writing traditional mathematical items (e.g. definitions, lemmas, theorems, proof steps, etc.) it also provides syntactic constructions to launch distinguished algorithms for processing particular mechanisms (e.g. term identifications, term reductions [4], flexary connectives [5]) increasing computational power of Verifier. The most interesting mechanism, from the point of view of this research, is the possibility of registering various properties of predicates and functors [6] at the stage of defining new notions. The current version of the Mizar system supports registration of reflexivity, irreflexivity, symmetry, asymmetry and connectedness for binary predicates; involutiveness and projectivity for unary operations; and commutativity and idempotence for binary operations. Table 1 presents how registrations of the properties are used in the MML and how they influence on proofs stored in the library. Consecutive columns show numbers of occurrences of each property, numbers of articles in which the properties were declared, numbers of errors occurring after removing registrations of the properties from texts, and numbers of articles with such errors.Footnote 1

Table 1. Properties of predicates and functors
Full size table

In this paper we propose strengthening of the Mizar system by processing of another common property used in mathematics – transitivity. It is described in Sect. 2. In Sect. 3 we present some results of our implementation and describe its potential influence on the MML. In Sect. 4 we indicate several directions of further development of processing properties in Mizar.

2 Transitivity

Transitivity is a very common property of predicates. It is a subject of research in various branches of mathematics. It is used to define, for example, orders, equivalences, etc. Many relations are tested to determine if they are transitive or not. Many mathematical theorems assert the transitivity of various relations.

We propose an enhancement of the Mizar system supporting automatic processing of transitive predicates, where by automatic we mean that some computations during the verification process are executed based on knowledge gathered in the MML which is not explicitly referred to in processed proof steps.Footnote 2 To enable such an automation, when a new predicate is defined, if it is transitive, it should be declared as transitive (just like in the case of other properties supported by the Mizar verifier [6]). Such a declaration has to be done within a definitional block with syntax

figure a

The correctness of the definition must be proven according to a special formula expressing the transitivity of the defined predicate. The formula is generated by the system. Having such a definition, whenever Verifier meets a conjunction of formulas \(\pi (a,b)\) and \(\pi (b,c)\) within an inference, the inference is enlarged by automatically generated formula \(\pi (a,c)\) which may help to justify the proof step. For example, when one wants to prove the transitivity of \(\texttt {<=}\) for real numbers, that is the statement \( \texttt {a<=b\, \& \,b<=c implies a<=c}\), Verifier (as a classical disprover) assumes three premises: \(\texttt {a<=b}\), \(\texttt {b<=c}\) and \(\texttt {a>c}\). Then, by transitivity, it knows that \(\texttt {a<=c}\) which contradicts with \(\texttt {a>c}\) and finishes the proof.

3 Experiments

The implemented software was tested on Mizar Version 8.1.02 working with the MML Version 5.36.1267.Footnote 3

An important part of the package is a tool (transdet) which detects theorems stored in the MML, that could be rewritten as registrations of the transitivity of some predicates (we will call such theorems transitivity-like theorems). In the current version of the library 127 such theorems were found in 90 articles. The Library Committee, who is responsible for the management, developing and revisions of the MML, will analyze all cases and decide which of them would be incorporated into the library. In the case of approval, a refactoring of the MML [9] will be required while maintaining licensing its content [10].

To present some examples detected in the MML Footnote 4 let us cite the transitivity of ordering of elements of a semilattice [11]

figure b

and the transitivity of being isomorphic groups [12]

figure c

An important gain from rewriting detected transitivity-like theorems as declarations of the transitivity of used predicates is decreasing the number of explicit references to the theorems from all proofs collected in the MML. Table 2 presents top 10 most cited such theorems.Footnote 5 These numbers mean that 16855 out of all 629048 (2.7 %) references in the entire library can be removed while ensuring that all proofs remain valid.

Table 2. References to transitivity-like theorems
Full size table

The software can be downloaded from http://alioth.uwb.edu.pl/~artur/transitivity.

4 Further Work

A possible direction to continue work is to implement processing of other commonly used in mathematics properties of relations, like, for example, antisymmetry, trichotomy, left- and right- Euclidean. Another topic is to introduce properties which are collections of other properties, like equivalence which is reflexive, symmetric and transitive; or preorder which is reflexive and transitive; etc. Of course, one may declare a relation as reflexive, symmetric and transitive, but it would be probably worth to enrich the Mizar language to make it closer and closer to traditional mathematical vernacular.

In the current stage of the Mizar system, all properties of predicates can be registered for binary predicates only. So, for example, the theorem [13]

figure d

is not transformable to a registration of transitivity, since the predicate reduces is ternary, not binary. But it is seen, that if we fix the value of one argument, the predicate can be understood as binary one, and we may think about its transitivity (or other properties of binary predicates). In general, properties dedicated for binary predicates, can be introduced for n-ary predicates, where \(2\le n\), with \(n-2\) fixed arguments.

5 Conclusions

In the paper we presented an extension of the Mizar system by introducing a new word to the Mizar language (transitivity) and new rules for processing transitive predicates. We detected theorems describing the transitivity of various relations gathered in the MML. It can be concluded that our implementation will have strong impact on the shape of many proofs – many explicit references to the theorems can be removed. It may even result in reorganization of proof steps within entire proofs [14].

As the last observation, it can be said that this new feature of the Mizar system was anticipated and expected by Mizar users. Josef Urban, in one of his papers [15], annotated a theorem as followsFootnote 6:

figure e