http://hdl.handle.net/11320/20996 2026-10-12T17:06:51Z 2026-10-12T17:06:51Z Bancerek, Grzegorz http://hdl.handle.net/11320/21033 2026-09-15T12:35:47Z 2008-01-01T00:00:00Z

Tytuł: Towards the Construction of a Model of Mizar Concepts Autorzy: Bancerek, Grzegorz Abstrakt: The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [14] and [13]. The theory here presented is an abstract of the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The base idea behind the formalization is dependence on variables which is determined by variable-dependence (variables may depend on other variables). The dependence constitutes a Galois connection between opposite poset of dependence-closed set of variables and the sup-semilattice of widening of Mizar types (smooth type widening). In the paper the concepts strictly connected with Mizar expressions are for malized. Among them are quasi-loci, quasi-terms, quasi-adjectives, and quasi types. The structural induction and operation of substitution are also introduced. The prefix quasi is used to indicate that some rules of construction of Mizar expressions may not be fulfilled. For example, variables, quasi-loci, and quasi terms have no assigned types and, in result, there is no possibility to conduct type-checking of arguments. The other gaps concern inconsistent and out-of context clusters of adjectives in types. Those rules are required in the Mizar identification process. However, the expression appearing in later processes of Mizar checker may not satisfy the rules. So, introduced apparatus is enough and adequate to describe data structures and algorithms from the Mizar checker (like equational classes).

2008-01-01T00:00:00Z Riccardi, Marco http://hdl.handle.net/11320/21032 2026-09-15T12:07:11Z 2008-01-01T00:00:00Z

Tytuł: Ramsey’s Theorem Autorzy: Riccardi, Marco Abstrakt: The goal of this article is to formalize two versions of Ramsey’s theorem. The theorems are not phrased in the usually pictorial representation of a coloured graph but use a set-theoretic terminology. After some useful lemma, the second section presents a generalization of Ramsey’s theorem on infinite set closely following the book [9]. The last section includes the formalization of the theorem in a more known version (see [1]).

2008-01-01T00:00:00Z Nakamura, Yatsuka Oniumi, Kunio Chang, Wenpai http://hdl.handle.net/11320/21029 2026-09-15T10:11:31Z 2008-01-01T00:00:00Z

Tytuł: Invertibility of Matrices of Field Elements Autorzy: Nakamura, Yatsuka; Oniumi, Kunio; Chang, Wenpai Abstrakt: In this paper the theory of invertibility of matrices of field elements (see e.g. [5], [6]) is developed. The main purpose of this article is to prove that the left invertibility and the right invertibility are equivalent for a matrix of field elements. To prove this, we introduced a special transformation of matrix to some canonical forms. Other concepts as zero vector and base vectors of field elements are also introduced as a preparation.

2008-01-01T00:00:00Z Bancerek, Grzegorz http://hdl.handle.net/11320/21028 2026-09-15T09:58:59Z 2008-01-01T00:00:00Z

Tytuł: Mizar Analysis of Algorithms: Algorithms over Integers Autorzy: Bancerek, Grzegorz Abstrakt: This paper is a continuation of [5] and concerns if-while algebras over integers. In these algebras the only elementary instructions are assign ment instructions. The instruction assigns to a (program) variable a value which is calculated for the current state according to some arithmetic expression. The expression may include variables, constants, and a limited number of arithmetic operations. States are functions from a given set of locations into integers. A variable is a function from the states into the locations and an expression is a function from the states into integers. Additional conditions (computabili ty) limit the set of variables and expressions and, simultaneously, allow to write algorithms in a natural way (and to prove their correctness). As examples the proofs of full correctness of two Euclid algorithms (with modulo operation and subtraction) and algorithm of exponentiation by squaring are given.

2008-01-01T00:00:00Z