## Summary

In the article we present in the Mizar system the catalogue of nine basic fuzzy implications, used especially in the theory of fuzzy sets. This work is a continuation of the development of fuzzy sets in Mizar; it could be used to give a variety of more general operations, and also it could be a good starting point towards the formalization of fuzzy logic (together with t-norms and t-conorms, formalized previously).

## Summary

In the article we continue in the Mizar system [8], [2] the formalization of fuzzy implications according to the monograph of Baczyński and Jayaram *“Fuzzy Implications”* [1]. We develop a framework of Mizar attributes allowing us for a smooth proving of basic properties of these fuzzy connectives [9]. We also give a set of theorems about the ordering of nine fundamental implications: Łukasiewicz (*I*
_{LK}), Gödel (*I*
_{GD}), Reichenbach (*I*
_{RC}), Kleene-Dienes (*I*
_{KD}), Goguen (*I*
_{GG}), Rescher (*I*
_{RS}), Yager (*I*
_{YG}), Weber (*I*
_{WB}), and Fodor (*I*
_{FD}).

This work is a continuation of the development of fuzzy sets in Mizar [6]; it could be used to give a variety of more general operations on fuzzy sets [13]. The formalization follows [10], [5], and [4].

## Summary

This paper continues formalization in Mizar , ] of basic notions of the composition-nominative approach to program semantics which was started in , .

The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [, , , , ].

In the paper we introduce a definition of the notion of a binominative function over a set *D* understood as a partial function which maps elements of *D* to *D*. The sets of binominative functions and nominative predicates over given sets form the carrier of the generalized Glushkov algorithmic algebra . This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.

We formalize the operations of this algebra (also called compositions) which are valid over uninterpretated data and which include among others the sequential composition, the prediction composition, the branching composition, the monotone Floyd-Hoare composition, and the cycle composition. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in , , .

## Summary

This paper continues formalization in the Mizar system , ] of basic notions of the composition-nominative approach to program semantics which was started in , , ].

The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. In particular, data in computer systems are modeled as nominative data . Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory , , , , ].

In the paper we give a formal definition of the notions of a binominative function over given sets of names and values (i.e. a partial function which maps simple-named complex-valued nominative data to such data) and a nominative predicate (a partial predicate on simple-named complex-valued nominative data). The sets of such binominative functions and nominative predicates form the carrier of the generalized Glushkov algorithmic algebra for simple-named complex-valued nominative data . This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties.

In particular, we formalize the operations of this algebra which require a specification of a data domain and which include the existential quantifier, the assignment composition, the composition of superposition into a predicate, the composition of superposition into a binominative function, the name checking predicate. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [, , ].

## Summary

In this paper we present a formalization in the Mizar system , ] of the correctness of the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers. The algorithm is written in terms of simple-named complex-valued nominative data , .

The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data . Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions , , , ].

## Summary

In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s

computing the factorial of given natural number n, where variables

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].

## Summary

This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:

i := val.1 j := val.2 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s

computing the natural n power of given complex number b, where variables

The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [14],[16],[7],[5].

## Abstract

Rough set theory is an important theory for the uncertain information processing. The information theoretic measures have been introduced into rough set theory and provided a new effective method in uncertainty measurement and attribute reduction. However, most of them did not consider the hierarchical structure of a decision table (D-Table). Thus, this paper concretely constructs three-way weighted combination-entropies based on the D-Table’s three-layer granular structures and Bayes’ theorem from a new perspective, and reveals the granulation monotonicity and systematic relationships of three-way weighted combination-entropies. The relevant conclusion provides a more complete and updated interpretation of granular computing for the uncertainty measurement, and it also establishes a more effective basis for the quantitative application in attribute reduction.

## Abstract

A notion for distance between hesitant fuzzy data is given. Using this new distance notion, we propose the technique for order preference by similarity to ideal solution for hesitant fuzzy sets and a new approach in modelling uncertainties. An illustrative example is constructed to show the feasibility and practicality of the new method.

## Summary

In the paper we give a formalization in the Mizar system , ] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in , ]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in .

We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true.

We formalize and prove the soundness of the rules of the inference system , ] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in .

The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data . Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in .