Semantics of MML Query - Ordering
Semantics of order directives of MML Query is presented. The formalization is done according to [1]
Analysis of Algorithms: An Example of a Sort Algorithm
We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.
Algebraic Approach to Algorithmic Logic
We introduce algorithmic logic - an algebraic approach according to [25]. It is done in three stages: propositional calculus, quantifier calculus with equality, and finally proper algorithmic logic. For each stage appropriate signature and theory are defined. Propositional calculus and quantifier calculus with equality are explored according to [24]. A language is introduced with language signature including free variables, substitution, and equality. Algorithmic logic requires a bialgebra structure...
Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm
Educational content for abstract reduction systems concerning reduction, convertibility, normal forms, divergence and convergence, Church- Rosser property, term rewriting systems, and the idea of the Knuth-Bendix Completion Algorithm. The theory is based on [1].
Term Context
Two construction functors: simple term with a variable and compound term with an operation and argument terms and schemes of term induction are introduced. The degree of construction as a number of used operation symbols is defined. Next, the term context is investigated. An x-context is a term which includes a variable x once only. The compound term is x-context iff the argument terms include an x-context once only. The context induction is shown and used many times. As a key concept, the context...
Mizar Analysis of Algorithms: Preliminaries
Algorithms and its parts - instructions - are formalized as elements of if-while algebras. An if-while algebra is a (1-sorted) universal algebra which has 4 operations: a constant - the empty instruction, a binary catenation of instructions, a ternary conditional instruction, and a binary while instruction. An execution function is defined on pairs (s, I), where s is a state (an element of certain set of states) and I is an instruction, and results in states. The execution function obeys control...
Representation Theorem for Stacks
In the paper the concept of stacks is formalized. As the main result the Theorem of Representation for Stacks is given. Formalization is done according to [13].
Towards the Construction of a Model of Mizar Concepts
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...
A Model of Mizar Concepts - Unification
The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [6] and [7]. The theory presented is an abstraction from the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The concepts formalized here are: standarized constructor signature, arity-rich signatures, and the unification of Mizar expressions.
Program Algebra over an Algebra
We introduce an algebra with free variables, an algebra with undefined values, a program algebra over a term algebra, an algebra with integers, and an algebra with arrays. Program algebra is defined as universal algebra with assignments. Programs depend on the set of generators with supporting variables and supporting terms which determine the value of free variables in the next state. The execution of a program is changing state according to successor function using supporting terms.
Sorting by Exchanging
We show that exchanging of pairs in an array which are in incorrect order leads to sorted array. It justifies correctness of Bubble Sort, Insertion Sort, and Quicksort.
Epsilon Numbers and Cantor Normal Form
An epsilon number is a transfinite number which is a fixed point of an exponential map: ωϵ = ϵ. The formalization of the concept is done with use of the tetration of ordinals (Knuth's arrow notation, ↑). Namely, the ordinal indexing of epsilon numbers is defined as follows: [...] and for limit ordinal λ: [...] Tetration stabilizes at ω: [...] Every ordinal number α can be uniquely written as [...] where κ is a natural number, n1, n2, …, nk are positive integers, and β1 > β2 > … > βκ are...
Free Term Algebras
We interoduce a new characterization of algebras of normal forms of term rewriting systems [35] as algerbras of term free in itself (any function from free generators into the algebra generates endomorphism of the algebra). Introduced algebras are free in classes of algebras satisfying some sets of equalities. Their universes are subsets of all terms and the denotations of operation symbols are partially identical with the operations of construction of terms. These algebras are compiler algebras...
Veblen Hierarchy
The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done...
Semantics of MML Query
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
Mizar Analysis of Algorithms: Algorithms over Integers
This paper is a continuation of [5] and concerns if-while algebras over integers. In these algebras the only elementary instructions are assignment 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...
On Multiset Ordering
Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M1 such that M1(x) > N1(x) and (∀y ∈ N1)x ⊀ y. It should be M1(x) ⩾ N1(x). Nevertheless we do not know whether x ∈ N1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].
Introduction to Matroids
The paper includes elements of the theory of matroids [23]. The formalization is done according to [12].MML identifier: MATROID0, version: 7.9.03 4.108.1028
Valuation Theory. Part I
In the article we introduce a valuation function over a field [1]. Ring of non negative elements and its ideal of positive elements have been also defined.
Page 1