Displaying 1921 – 1940 of 4962

Showing per page

Formalization of Generalized Almost Distributive Lattices

Adam Grabowski (2014)

Formalized Mathematics

Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative...

Formalization of Provenes fuzzy functional dependency in fuzzy databases.

Nedzad Dukic, Zikrija Avdagic (2004)

Mathware and Soft Computing

In this paper we establish equivalence between a theory of fuzzy functional dependences and a fragment of fuzzy logic. We give a way to interpret fuzzy functional dependences as formulas in fuzzy logic. This goal is realized in a few steps. Truth assignment of attributes is defined in terms of closeness between two tuples in a fuzzy relation. A corresponding fuzzy formula is associated to a fuzzy functional dependence. It is proved that if a relation satisfies a fuzzy functional dependence, then...

Formalization of the Advanced Encryption Standard. Part I

Kenichi Arai, Hiroyuki Okazaki (2013)

Formalized Mathematics

In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify...

Formally certified floating-point filters for homogeneous geometric predicates

Guillaume Melquiond, Sylvain Pion (2007)

RAIRO - Theoretical Informatics and Applications

Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this...

Formulation of Cell Petri Nets

Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama (2013)

Formalized Mathematics

Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...

Fractal representation of the attractive lamination of an automorphism of the free group

Pierre Arnoux, Valérie Berthé, Arnaud Hilion, Anne Siegel (2006)

Annales de l’institut Fourier

In this paper, we extend to automorphisms of free groups some results and constructions that classically hold for morphisms of the free monoid, i.e., the so-called substitutions. A geometric representation of the attractive lamination of a class of automorphisms of the free group (irreducible with irreducible powers (iwip) automorphisms) is given in the case where the dilation coefficient of the automorphism is a unit Pisot number. The shift map associated with the attractive symbolic lamination...

Currently displaying 1921 – 1940 of 4962