The Dialectica interpretation of first-order classical affine logic.
The diophantine theory of a ring of analytic functions.
The elementary theory of Abelian groups with m-chains of pure subgroups
The elimination of descriptions from A. Bressan’s modal language on which the logical calculus is based
The First Isomorphism Theorem and Other Properties of Rings
Different properties of rings and fields are discussed [12], [41] and [17]. We introduce ring homomorphisms, their kernels and images, and prove the First Isomorphism Theorem, namely that for a homomorphism f : R → S we have R/ker(f) ≅ Im(f). Then we define prime and irreducible elements and show that every principal ideal domain is factorial. Finally we show that polynomial rings over fields are Euclidean and hence also factorial
The First Mean Value Theorem for Integrals
In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.MML identifier: MESFUNC7, version: 7.8.09 4.97.1001
The Formal Construction of Fuzzy Numbers
In this article, we continue the development of the theory of fuzzy sets [23], started with [14] with the future aim to provide the formalization of fuzzy numbers [8] in terms reflecting the current state of the Mizar Mathematical Library. Note that in order to have more usable approach in [14], we revised that article as well; some of the ideas were described in [12]. As we can actually understand fuzzy sets just as their membership functions (via the equality of membership function and their set-theoretic...
The Formalization of Decision-Free Petri Net
In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. Then we formalize the concept of directed path and directed circuit nets in Petri nets to prove properties of DFPN. We also present the definition of firing transitions and transition sequences with natural numbers marking that always check whether transition is enabled or not and after firing it only removes the available tokens (i.e., it does not remove from zero number of tokens). At the end of this...
The Heyting doctrines
The internal and external aspect of logic and set theory in elementary topoi
The interpreted type-free modal calculus
The interpreted type-free modal calculus
The interpreted type-free modal calculus . II
The irrelevant information principle for collective probabilistic reasoning
Within the framework of discrete probabilistic uncertain reasoning a large literature exists justifying the maximum entropy inference process, , as being optimal in the context of a single agent whose subjective probabilistic knowledge base is consistent. In particular Paris and Vencovská completely characterised the inference process by means of an attractive set of axioms which an inference process should satisfy. More recently the second author extended the Paris-Vencovská axiomatic approach...
The join of equational theories
The -theory of profinite abelian groups
The lattice of bi-numerations of arithmetic. I.
The lattice of bi-numerations of arithmetic. II.
The lattice of linear classes in prime-valued logics
The lattices of numerations of theories containing Peano's arithmetic