Displaying 201 – 220 of 1306

Showing per page

Compactness in Metric Spaces

Kazuhisa Nakasho, Keiko Narita, Yasunari Shidama (2016)

Formalized Mathematics

In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness,...

Comparing the succinctness of monadic query languages over finite trees

Martin Grohe, Nicole Schweikardt (2004)

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

We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog. Succinctness...

Comparing the succinctness of monadic query languages over finite trees

Martin Grohe, Nicole Schweikardt (2010)

RAIRO - Theoretical Informatics and Applications

We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog.
Succinctness...

Complexity of λ -term reductions

M. Dezani-Ciancaglini, S. Ronchi Della Rocca, L. Saitta (1979)

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

Conservation Rules of Direct Sum Decomposition of Groups

Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama (2016)

Formalized Mathematics

In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.

Considering uncertainty and dependence in Boolean, quantum and fuzzy logics

Mirko Navara, Pavel Pták (1998)

Kybernetika

A degree of probabilistic dependence is introduced in the classical logic using the Frank family of t -norms known from fuzzy logics. In the quantum logic a degree of quantum dependence is added corresponding to the level of noncompatibility. Further, in the case of the fuzzy logic with P -states, (resp. T -states) the consideration turned out to be fully analogous to (resp. considerably different from) the classical situation.

Constructing Binary Huffman Tree

Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama (2013)

Formalized Mathematics

Huffman coding is one of a most famous entropy encoding methods for lossless data compression [16]. JPEG and ZIP formats employ variants of Huffman encoding as lossless compression algorithms. Huffman coding is a bijective map from source letters into leaves of the Huffman tree constructed by the algorithm. In this article we formalize an algorithm constructing a binary code tree, Huffman tree.

Construction methods for implications on bounded lattices

M. Nesibe Kesicioğlu (2019)

Kybernetika

In this paper, the ordinal sum construction methods of implications on bounded lattices are studied. Necessary and sufficient conditions of an ordinal sum for obtaining an implication are presented. New ordinal sum construction methods on bounded lattices which generate implications are discussed. Some basic properties of ordinal sum implications are studied.

Currently displaying 201 – 220 of 1306