Browse

You are looking at 41 - 50 of 681 items for :

  • Algebra and Number Theory x
Clear All
Open access

Ievgen Ivanov, Artur Korniłowicz and Mykola Nikitchenko

Summary

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

We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] 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 [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3].

The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. 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 [8].

Open access

Adam Grabowski and Michał Sielwiesiuk

Summary

Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article we give the formal characterization of two closely related rough approximations, along the lines proposed in a paper by Gomolińska [2]. We continue the formalization of rough sets in Mizar [1] started in [6].

Open access

Marcin Acewicz and Karol Pąk

Summary

The main purpose of formalization is to prove that two equations ya(z)= y, y = xz are Diophantine. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.

In our previous work [6], we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities. In this formalization, we express these relations in terms of Diophantine set introduced in [7]. We prove that these relations are Diophantine and then we prove several second-order theorems that provide the ability to combine Diophantine relation using conjunctions and alternatives as well as to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation. Finally, we investigate the possibilities of our approach to prove that the two equations, being the main purpose of this formalization, are Diophantine.

The formalization by means of Mizar system [3], [2] follows Z. Adamowicz, P. Zbierski [1] as well as M. Davis [4].

Open access

Sebastian Koch

Summary

In the previous article [5] supergraphs and several specializations to formalize the process of drawing graphs were introduced. In this paper another such operation is formalized in Mizar [1], [2]: drawing a vertex and then immediately drawing edges connecting this vertex with a subset of the other vertices of the graph. In case the new vertex is joined with all vertices of a given graph G, this is known as the join of G and the trivial loopless graph K 1. While the join of two graphs is known and found in standard literature (like [9], [4], [8] and [3]), the operation discribed in this article is not.

Alongside the new operation a mode to reverse the directions of a subset of the edges of a graph is introduced. When all edge directions of a graph are reversed, this is commonly known as the converse of a (directed) graph.

Open access

Sebastian Koch

Summary

Drawing a finite graph is usually done by a finite sequence of the following three operations.

1. Draw a vertex of the graph.

2. Draw an edge between two vertices of the graph.

3. Draw an edge starting from a vertex of the graph and immediately draw a vertex at the other end of it.

By this procedure any finite graph can be constructed. This property of graphs is so obvious that the author of this article has yet to find a reference where it is mentioned explicitly. In introductionary books (like [10], [5], [9]) as well as in advanced ones (like [4]), after the initial definition of graphs the examples are usually given by graphical representations rather than explicit set theoretic descriptions, assuming a mutual understanding how the representation is to be translated into a description fitting the definition. However, Mizar [2], [3] does not possess this innate ability of humans to translate pictures into graphs. Therefore, if one wants to create graphs in Mizar without directly providing a set theoretic description (i.e. using the createGraph functor), a rigorous approach to the constructing operations is required.

In this paper supergraphs are defined as an inverse mode to subgraphs as given in [8]. The three graph construction operations are defined as modes extending Supergraph similar to how the various remove operations were introduced as submodes of Subgraph in [8]. Many theorems are proven that describe how graph properties are transferred to special supergraphs. In particular, to prove that disconnected graphs cannot become connected by adding an edge between two vertices that lie in the same component, the theory of replacing a part of a walk with another walk is introduced in the preliminaries.

Open access

Athanasios Sourmelidis

Abstract

In this paper, we prove a discrete analogue of Voronin’s early finite-dimensional approximation result with respect to terms from a given Beatty sequence and make use of Taylor approximation in order to derive a weak universality statement.

Open access

Ramesh Sirisetti and G. Jogarao

Abstract

In this paper, the concept of relative complementation in almost distributive lattice is generalized. We obtain several properties on the sets of weak relative complement elements. We prove a sufficient condition for a weakly relatively complemented almost distributive lattice with dense elements to become a generalized stone almost distributive lattice.

Open access

Arpita Das and Pratima Panigrahi

Abstract

The R-graph R(G) of a graph G is the graph obtained from G by intro- ducing a new vertex ue for each e ∈ E(G) and making ue adjacent to both the end vertices of e. In this paper, we determine the adjacency, Lapla- cian and signless Laplacian spectra of R-vertex join and R-edge join of a connected regular graph with an arbitrary regular graph in terms of their eigenvalues. Moreover, applying these results we construct some non-regular A-cospectral, L-cospectral and Q-cospectral graphs, and find the number of spanning trees.

Open access

Akbar Rezaei and Arsham Borumand Saeid

Abstract

Hilbert algebras are important tools for certain investigations in algebraic logic since they can be considered as fragments of any propositional logic containing a logical connective implication and the constant 1 which is considered as the logical value “true” and as a generalization of this was defined the notion of g-Hilbert algebra. In this paper, we investigate the relationship between g-Hilbert algebras, gi-algebras, implication gruopoid and BE-algebras. In fact, we show that every g-Hilbert algebra is a self distributive BE-algebras and conversely. We show cannot remove the condition self distributivity. Therefore we show that any self distributive commutative BE-algebras is a gi-algebra and any gi-algebra is strong and transitive if and only if it is a commutative BE-algebra. We prove that the MV -algebra is equivalent to the bounded commutative BE-algebra.

Open access

Martine Queffélec

Abstract

We intend to unroll the surprizing properties of the Thue-Morse sequence with a harmonic analysis point of view, and mention in passing some related open questions.