Algèbre du calcul propositionnel trivalent de Heyting
In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real...
We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.
This paper has three parts. First, we study and characterize amenable and extremely amenable topological semigroups in terms of invariant measures using integral logic. We prove definability of some properties of a topological semigroup such as amenability and the fixed point on compacta property. Second, we define types and develop local stability in the framework of integral logic. For a stable formula ϕ, we prove definability of all complete ϕ-types over models and deduce from this the fundamental...
We introduce Kleene's 3-valued logic in a language containing, besides the Boolean connectives, a constant for the undefined truth value, so in developing semantics we can switch from the usual treatment based on DM-algebras to the narrower class of DMF-algebras (De Morgan algebras with a single fixed point for negation). A sequent calculus for Kleene's logic is introduced and proved complete with respect to threevalent semantics. The completeness proof is based on a version of the prime ideal...
This paper deals with the problem of the determination of lower solutions of fuzzy relational equations. An algorithm of calculation of such a solution is presented.
In this paper, we propose a novel approach for solving a fuzzy bi-objective multi-index fixed-charge transportation problem where the aim is to minimize two objectives: the total transportation cost and transportation time. The parameters of the problem, such as fixed cost, variable cost, and transportation time are represented as fuzzy numbers. To extract crisp values from these parameters, a linear ranking function is used. The proposed approach initially separates the main problem into sub-problems....
We present an axiom system for class of full Euclidean spaces (i.e. of projective closures of Euclidean spaces) and prove the representation theorem for our system, using connections between Euclidean spaces and elliptic planes.
Incidence spatial geometry is based on three-sorted structures consisting of points, lines and planes together with three intersort binary relations between points and lines, lines and planes and points and planes. We introduce an equivalent one-sorted geometrical structure, called incidence spatial frame, which is suitable for modal considerations. We are going to prove completeness by SD-Theorem. Extensions to projective, affine and hyperbolic geometries are also considered.
Hyperbolic projective-metric planes, first axiomatized by R. Lingenberg [7], are shown to be axiomatizable in terms of lines and orthogonality.