All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 42 Next

Displaying 821 – 840 of 1313

Showing per page

Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem

Marco Caminati (2011)

Formalized Mathematics

Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster registrations...

Simple games in Łukasiewicz calculus and their cores

Petr Cintula, Tomáš Kroupa (2013)

Kybernetika

We propose a generalization of simple coalition games in the context of games with fuzzy coalitions. Mimicking the correspondence of simple games with non-constant monotone formulas of classical logic, we introduce simple Łukasiewicz games using monotone formulas of Łukasiewicz logic, one of the most prominent fuzzy logics. We study the core solution on the class of simple Łukasiewicz games and show that cores of such games are determined by finitely-many linear constraints only. The non-emptiness...

S-implications and R -implications on a finite chain

Margarita Mas, Miquel Monserrat, Joan Torrens (2004)

Kybernetika

This paper is devoted to the study of two kinds of implications on a finite chain L : S -implications and R -implications. A characterization of each kind of these operators is given and a lot of different implications on L are obtained, not only from smooth t-norms but also from non smooth ones. Some additional properties on these implications are studied specially in the smooth case. Finally, a class of non smooth t-norms including the nilpotent minimum is characterized. Any t-norm in this class...

Smooth and sharp thresholds for random k -XOR-CNF satisfiability

Nadia Creignou, Hervé Daudé (2003)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

The aim of this paper is to study the threshold behavior for the satisfiability property of a random k -XOR-CNF formula or equivalently for the consistency of a random Boolean linear system with k variables per equation. For k ≥ 3 we show the existence of a sharp threshold for the satisfiability of a random k -XOR-CNF formula, whereas there are smooth thresholds for k = 1 and k = 2 .

Smooth implications on a finite chain

Yong Su (2019)

Kybernetika

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.

Sobre funciones de negación en la teoría de conjuntos difusos.

Enric Trillas (1979)

Stochastica

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

Miguel-Ángel Sicilia, Juan-J. Cuadrado-Gallego, Javier Crespo, Elena García Barriocanal (2005)

Kybernetika

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 word equations

Habib Abdulrab (1990)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Some Algebraic Properties of Polynomial Rings

Christoph Schwarzweller, Artur Korniłowicz (2016)

Formalized Mathematics

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

Jaroslav Ježek (1999)

Czechoslovak Mathematical Journal

Let W be the free monoid over a finite alphabet A . We prove that a congruence of W generated by a finite number of pairs 〈 a u , u 〉 , where a ∈ A and u ∈ W , is always decidable.

Some decidable theories with finitely many covers which are decidable and algorithmically found

Cornelia Kalfa (1994)

Colloquium Mathematicae

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

Roland Coghetto (2014)

Formalized Mathematics

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 key research problems in automated theorem proving for hardware and software verification.

Matt Kaufmann, J. Strother Moore (2004)

RACSAM

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

Gül Deniz Çaylı (2019)

Kybernetika

In this study, we introduce new methods for constructing t-norms and t-conorms on a bounded lattice L based on a priori given t-norm acting on [ a , 1 ] and t-conorm acting on [ 0 , a ] for an arbitrary element a ∈ L ∖ { 0 , 1 } . 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.

Currently displaying 821 – 840 of 1313