The aim of this paper is to study the threshold behavior for the satisfiability property of a random -XOR-CNF formula or equivalently for the consistency of a random Boolean linear system with variables per equation. For we show the existence of a sharp threshold for the satisfiability of a random -XOR-CNF formula, whereas there are smooth thresholds for and .
Mas et al. adapted the notion of smoothness, introduced by Godo and Sierra, and discussed two kinds of smooth implications (a discrete counterpart of continuous fuzzy implications) on a finite chain. This work is devoted to exploring the formal relations between smoothness and other six properties of implications on a finite chain. As a byproduct, several classes of smooth implications on a finite chain are characterized.
En su trabajo de 1973, ya clásico, Bellman y Giertz probaron que P(X) es un retículo distributivo con máximo y mínimo sólo (con hipótesis muy razonables) bajo las usuales definiciones (A U B)(x) = máx {A(x),B(x)}, (A ∩ B)(x) = mín {A(x),B(x)}, tratando escasamente el formalismo analítico relativo a la negación. En el presente trabajo se prueba que tal P(X) es un álgebra de DeMorgan si y sólo si la función de negación posee generador aditivo y que tales negaciones constituyen, en un cierto grupo...
Parametric software cost estimation models are well-known and widely used estimation tools, and several fuzzy extensions have been proposed to introduce a explicit handling of imprecision and uncertainty as part of them. Nonetheless, such extensions do not consider two basic facts that affect the inputs of software cost parametric models: cost drivers are often expressed through vague linguistic categories, and in many cases cost drivers are better expressed in terms of aggregations of second-level...
In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/ is isomorphic to the field of polynomials with degree smaller than the one of p.
Let be the free monoid over a finite alphabet . We prove that a congruence of generated by a finite number of pairs , where and , is always decidable.
In any recursive algebraic language, I find an interval of the lattice of equational theories, every element of which has finitely many covers. With every finite set of equations of this language, an equational theory of this interval is associated, which is decidable with decidable covers that can be algorithmically found. If the language is finite, both this theory and its covers are finitely based. Also, for every finite language and for every natural number n, I construct a finitely based decidable...
We calculate the values of the trigonometric functions for angles: [XXX] , by [16]. After defining some trigonometric identities, we demonstrate conventional trigonometric formulas in the triangle, and the geometric property, by [14], of the triangle inscribed in a semicircle, by the proposition 3.31 in [15]. Then we define the diameter of the circumscribed circle of a triangle using the definition of the area of a triangle and prove some identities of a triangle [9]. We conclude by indicating that...
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...
In this study, we introduce new methods for constructing t-norms and t-conorms on a bounded lattice based on a priori given t-norm acting on and t-conorm acting on for an arbitrary element . We provide an illustrative example to show that our construction methods differ from the known approaches and investigate the relationship between them. Furthermore, these methods are generalized by iteration to an ordinal sum construction for t-norms and t-conorms on a bounded lattice.
In this paper, we introduce the product, coproduct, equalizer and coequalizer notions on the category of fuzzy implications on a bounded lattice that results in the existence of the limit, pullback, colimit and pushout. Also isomorphism, monic and epic are introduced in this category. Then a subcategory of this category, called the skeleton, is studied. Where none of any two fuzzy implications are -conjugate.
In this paper, an equivalence on the class of uninorms on a bounded lattice is discussed. Some relationships between the equivalence classes of uninorms and the equivalence classes of their underlying t-norms and t-conorms are presented. Also, a characterization for the sets admitting some incomparability w.r.t. the U-partial order is given.
This article describes some properties of p-groups and some properties of commutative p-groups.
We investigate some (universal algebraic) properties of residuated lattices—algebras which play the role of structures of truth values of various systems of fuzzy logic.
We consider properties of state filters of state residuated lattices and prove that for every state filter of a state residuated lattice :
We first provide a modified version of the proof in [3] that the Sorgenfrey line is T1. Here, we prove that it is in fact T2, a stronger result. Next, we prove that all subspaces of ℝ1 (that is the real line with the usual topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey line is Lindel¨of, which is based on the proof found in [8]. Next, we construct the Sorgenfrey plane, as the product topology of the Sorgenfrey line and itself. We prove that the Sorgenfrey plane...