Sober spaces and continuations.
Sobre funciones de negación en la teoría de conjuntos difusos.
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...
Software cost estimation with fuzzy inputs: Fuzzy modelling and aggregation of cost drivers
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...
Solving algebraic problems in propositional logic by tableau.
Solving word equations
Some Algebraic Properties of Polynomial Rings
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.
Some decidable congruences of free monoids
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.
Some decidable theories with finitely many covers which are decidable and algorithmically found
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...
Some Facts about Trigonometry and Euclidean Geometry
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...
Some generalizations to two systems of set theory based on combinatory logic.
Some key research problems in automated theorem proving for hardware and software verification.
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,...
Some methods to obtain t-norms and t-conorms on bounded lattices
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.
Some notes on the category of fuzzy implications on bounded lattices
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.
Some notes on U-partial order
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.
Some Properties of p -Groups and Commutative p -Groups
This article describes some properties of p-groups and some properties of commutative p-groups.
Some properties of residuated lattices
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.
Some properties of state filters in state residuated lattices
We consider properties of state filters of state residuated lattices and prove that for every state filter of a state residuated lattice :
Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane
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...
Some Remarkable Identities Involving Numbers
The article focuses on simple identities found for binomials, their divisibility, and basic inequalities. A general formula allowing factorization of the sum of like powers is introduced and used to prove elementary theorems for natural numbers. Formulas for short multiplication are sometimes referred in English or French as remarkable identities. The same formulas could be found in works concerning polynomial factorization, where there exists no single term for various identities. Their usability...
Some remarks about the connections between combinatory logic and axiomatic recursion theory.