The Mizar Home PageAbstract. Bezier curves were introduced not so many years ago, in the sixties. Immediately, they were used across the computer scene. Bezier curves of the 3rd degree were included into the PostScript language (commands: curveto, rcurveto). They are now present in each printed document. We ask two questions: (1) why are Bezier curves so popular? (2) do we know everything about Bezier curves?
As well as the theory of Bezier curves, the article explores a new concept of software proofs. An author of a paper creates software which illustrates the theory considered in the paper. In certain cases the software can prove theorems from the paper. The software must be attached to the paper in open format, i.e. complete source code of the software. A reader opens the software utilizing the Microsoft Visual Basic - probably the most popular compiler at the moment. 4th August 2001
[Download PostScript = 61.8 kb]
Abstract. Tarski Grothendieck axiom states that "everything is a set". Kuratowski Zorn lemma helps to overcome cardinality problems. This article presents definitions of a collection of bits, B-bit numbers, set-like binary representation. The last definition is then compared to the standard binary representation. The fundamentals of Binary Arithmetic are presented, but all operations on bits are regarded as sets. One-placed and two-placed operations on bits as well as their compositions are given as samples. Several propositions, regarding operations as sets, are listed. Finally, one-placed and two-placed bitwise operations on B-bit numbers are explained. As a result of the discussion in this paper, we can say that the addition of numbers is an 8-element set. Who said that numbers are a result of counting? How to count if we have no numbers? Numbers are well ordered pieces of a universal set. Moreover, they are probably well ordered by time. 7th May 2001
[Download PostScript = 53.5 kb]
Abstract. Petri Nets concept is well known and widely used. Encapsulated Petri Nets, if applied, could change computer software drastically. To be able to define extended Petri Nets and then encapsulated Petri Nets, the basic definition of the concept had to be simplified. The new definition is equivalent to the functions, procedures, and finally, with other Petri Nets. The addition of numbers is given as a sample. If Encapsulated Petri Nets can add numbers, they will do everything. 29th April 2001
[Download PostScript = 46.6 kb]
The Mizar Home Page