Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 19

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

A Model of Mizar Concepts - Unification

100%
Bancerek G.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
65-75
EN
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.
2
Content available remote

Representation Theorem for Stacks

100%
Bancerek G.
Formalized Mathematics
|
2011
|
tom 19
|
nr 4
241-250
EN
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].
3
Content available remote

Semantics of MML Query

100%
Bancerek G.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
147-155
EN
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
4
Content available remote

Mizar Analysis of Algorithms: Preliminaries

100%
Bancerek G.
Formalized Mathematics
|
2007
|
tom 15
|
nr 3
87-110
EN
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 structures using the set of distinguished true states, i.e. a condition instruction is executed and the continuation of execution depends on if the resulting state is in true states or not. Termination is also defined for pairs (s, I) and depends on the execution function. The existence of execution function determined on elementary instructions and its uniqueness for terminating instructions are shown.
5
Content available remote

Algebraic Approach to Algorithmic Logic

100%
Bancerek G.
Formalized Mathematics
|
2014
|
tom 22
|
nr 3
225-255
EN
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 which is an extension of language signature and program algebra. While-if algebra of generator set and algebraic signature is bialgebra with appropriate properties and is used as basic type of algebraic logic.
6
Content available remote

Term Context

100%
Bancerek G.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
125-155
EN
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 substitution is introduced. Finally, the translations and endomorphisms are expressed by context substitution.
7
Content available remote

Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm

100%
Bancerek G.
Formalized Mathematics
|
2014
|
tom 22
|
nr 1
37-56
EN
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].
8
Content available remote

On Multiset Ordering

100%
Bancerek G.
Formalized Mathematics
|
2016
|
tom 24
|
nr 2
95-106
EN
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].
9
Content available remote

Free Term Algebras

100%
Bancerek G.
Formalized Mathematics
|
2012
|
tom 20
|
nr 3
239-256
EN
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 requiring some equalities of terms, e.g., associativity of addition.
10
Content available remote

Sorting by Exchanging

100%
Bancerek G.
Formalized Mathematics
|
2011
|
tom 19
|
nr 2
93-102
EN
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.
11
Content available remote

Veblen Hierarchy

100%
Bancerek G.
Formalized Mathematics
|
2011
|
tom 19
|
nr 2
83-92
EN
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 with use of universal sets (Tarski classes). Namely, we define the Veblen functions in a given universal set and φα(β) as a value of Veblen function from the smallest universal set including α and β.
12
Content available remote

Analysis of Algorithms: An Example of a Sort Algorithm

100%
Bancerek G.
Formalized Mathematics
|
2013
|
tom 21
|
nr 1
1-23
EN
We analyse three algorithms: exponentiation by squaring, calculation of maximum, and sorting by exchanging in terms of program algebra over an algebra.
13
Content available remote

Semantics of MML Query - Ordering

100%
Bancerek G.
Formalized Mathematics
|
2013
|
tom 21
|
nr 1
41-46
EN
Semantics of order directives of MML Query is presented. The formalization is done according to [1]
14
Content available remote

Mizar Analysis of Algorithms: Algorithms over Integers

100%
Bancerek G.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
177-194
EN
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 into the locations and an expression is a function from the states into integers. Additional conditions (computability) 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.MML identifier: AOFA I00, version: 7.8.10 4.100.1011
15
Content available remote

Epsilon Numbers and Cantor Normal Form

100%
Bancerek G.
Formalized Mathematics
|
2009
|
tom 17
|
nr 4
249-256
EN
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 ordinal numbers (βκ = 0). This decomposition of α is called the Cantor Normal Form of α.
16
Content available remote

Towards the Construction of a Model of Mizar Concepts

100%
Bancerek G.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
207-230
EN
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 formalized. 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).MML identifier: ABCMIZ 1, version: 7.9.01 4.101.1015
17
Content available remote

Program Algebra over an Algebra

100%
Bancerek G.
Formalized Mathematics
|
2012
|
tom 20
|
nr 4
309-341
EN
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.
18
Content available remote

Introduction to Matroids

64%
Bancerek G., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
325-332
EN
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
19
Content available remote

Valuation Theory. Part I

52%
Bancerek G., Kobayashi H., Korniłowicz A.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
7-14
EN
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.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.