Displaying 981 – 1000 of 1313

Showing per page

Topologies, Continuity and Bisimulations

J. M. Davoren (2010)

RAIRO - Theoretical Informatics and Applications

The notion of a bisimulation relation is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of hybrid control systems, where system properties are expressible by formulas of the modal μ-calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some...

Topology from Neighbourhoods

Roland Coghetto (2015)

Formalized Mathematics

Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this...

Torsion Part of ℤ-module

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2015)

Formalized Mathematics

In this article, we formalize in Mizar [7] the definition of “torsion part” of ℤ-module and its properties. We show ℤ-module generated by the field of rational numbers as an example of torsion-free non free ℤ-modules. We also formalize the rank-nullity theorem over finite-rank free ℤ-modules (previously formalized in [1]). ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [23] and cryptographic systems with lattices [24].

Torsion Z-module and Torsion-free Z-module

Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama (2014)

Formalized Mathematics

In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].

Totally coherent set-valued probability assessments

Angelo Gilio, Salvatore Ingrassia (1998)

Kybernetika

We introduce the concept of total coherence of a set-valued probability assessment on a family of conditional events. In particular we give sufficient and necessary conditions of total coherence in the case of interval-valued probability assessments. Some relevant cases in which the set-valued probability assessment is represented by the unitary hypercube are also considered.

Towards an extension of the 2-tuple linguistic model to deal with unbalanced linguistic term sets

Mohammed-Amine Abchir, Isis Truck (2013)

Kybernetika

In the domain of Computing with words (CW), fuzzy linguistic approaches are known to be relevant in many decision-making problems. Indeed, they allow us to model the human reasoning in replacing words, assessments, preferences, choices, wishes... by ad hoc variables, such as fuzzy sets or more sophisticated variables. This paper focuses on a particular model: Herrera and Martínez' 2-tuple linguistic model and their approach to deal with unbalanced linguistic term sets. It is interesting since the...

Traced premonoidal categories

Nick Benton, Martin Hyland (2003)

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

Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show that in a Freyd category, these notions are equivalent, generalizing a well-known theorem relating traces and Conway operators in cartesian categories.

Traced Premonoidal Categories

Nick Benton, Martin Hyland (2010)

RAIRO - Theoretical Informatics and Applications

Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show that in a Freyd category, these notions are equivalent, generalizing a well-known theorem relating traces and Conway operators in Cartesian categories.

Trames, classifications, définitions

Daniel Parrochia (1991)

Mathématiques et Sciences Humaines

L'article part d'une analogie entre trames et partitions, définitions conceptuelles et optiques. On montre que les divisions d'un espace de concepts ressemblent souvent à celles de l'espace réel. On étudie alors quelques exemples de pavage d'un espace conceptuel (Aristote) et on compare les processus dichotomiques platoniciens (générateurs de définitions) aux filtres d'une algèbre booléenne. Par la suite, on généralise ces modèles, considérant des structures floues et des «ensembles approximatifs»...

Two Axiomatizations of Nelson Algebras

Adam Grabowski (2015)

Formalized Mathematics

Nelson algebras were first studied by Rasiowa and Białynicki- Birula [1] under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and [2] the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper [14] on constructive logic with strong negation. By a Nelson algebra we mean an abstract algebra 〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉 where L is the carrier, − is a quasi-complementation (Rasiowa used...

Two extensions of system F with (co)iteration and primitive (co)recursion principles

Favio Ezequiel Miranda-Perea (2009)

RAIRO - Theoretical Informatics and Applications

This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism....

Currently displaying 981 – 1000 of 1313