Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Dilworth's Decomposition Theorem for Posets

100%
Rudnicki P.
Formalized Mathematics
|
2009
|
tom 17
|
nr 4
223-232
EN
The following theorem is due to Dilworth [8]: Let P be a partially ordered set. If the maximal number of elements in an independent subset (anti-chain) of P is k, then P is the union of k chains (cliques).In this article we formalize an elegant proof of the above theorem for finite posets by Perles [13]. The result is then used in proving the case of infinite posets following the original proof of Dilworth [8].A dual of Dilworth's theorem also holds: a poset with maximum clique m is a union of m independent sets. The proof of this dual fact is considerably easier; we follow the proof by Mirsky [11]. Mirsky states also a corollary that a poset of r x s + 1 elements possesses a clique of size r + 1 or an independent set of size s + 1, or both. This corollary is then used to prove the result of Erdős and Szekeres [9].Instead of using posets, we drop reflexivity and state the facts about anti-symmetric and transitive relations.
2
Content available remote

Simple Graphs as Simplicial Complexes: the Mycielskian of a Graph

64%
Rudnicki P., Stewart L.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
161-174
EN
Harary [10, p. 7] claims that Veblen [20, p. 2] first suggested to formalize simple graphs using simplicial complexes. We have developed basic terminology for simple graphs as at most 1-dimensional complexes. We formalize this new setting and then reprove Mycielski’s [12] construction resulting in a triangle-free graph with arbitrarily large chromatic number. A different formalization of similar material is in [15].
3
Content available remote

Chordal Graphs

64%
Arneson B., Rudnicki P.
Formalized Mathematics
|
2006
|
tom 14
|
nr 3
79-92
EN
We are formalizing [9, pp. 81-84] where chordal graphs are defined and their basic characterization is given. This formalization is a part of the M.Sc. work of the first author under supervision of the second author.
4
Content available remote

Helly Property for Subtrees

64%
Enright J., Rudnicki P.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
91-96
EN
We prove, following [5, p. 92], that any family of subtrees of a finite tree satisfies the Helly property.MML identifier: HELLY, version: 7.8.09 4.97.1001
5
Content available remote

Recognizing Chordal Graphs: Lex BFS and MCS1

64%
Arneson B., Rudnicki P.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
187-206
EN
We are formalizing the algorithm for recognizing chordal graphs by lexicographic breadth-first search as presented in [13, Section 3 of Chapter 4, pp. 81-84]. Then we follow with a formalization of another algorithm serving the same end but based on maximum cardinality search as presented by Tarjan and Yannakakis [25].This work is a part of the MSc work of the first author under supervision of the second author. We would like to thank one of the anonymous reviewers for very useful suggestions.
6
Content available remote

Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane

64%
Arnaud A. S., Rudnicki P.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
83-85
EN
I would like to thank Piotr Rudnicki for taking me on as his summer student and being a mentor to me. Piotr was an incredibly caring, intelligent, funny, passionate human being. I am proud to know I was his last student, in a long line of students he has mentored and cared about throughout his life. Thank you Piotr, for the opportunity you gave me, and for the faith, confidence and trust you showed in me. I will miss you.
7
Content available remote

The Mycielskian of a Graph

64%
Rudnicki P., Stewart L.
Formalized Mathematics
|
2011
|
tom 19
|
nr 1
27-34
EN
Let ω(G) and χ(G) be the clique number and the chromatic number of a graph G. Mycielski [11] presented a construction that for any n creates a graph Mn which is triangle-free (ω(G) = 2) with χ(G) > n. The starting point is the complete graph of two vertices (K2). M(n+1) is obtained from Mn through the operation μ(G) called the Mycielskian of a graph G.We first define the operation μ(G) and then show that ω(μ(G)) = ω(G) and χ(μ(G)) = χ(G) + 1. This is done for arbitrary graph G, see also [10]. Then we define the sequence of graphs Mn each of exponential size in n and give their clique and chromatic numbers.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.