10.06.2015, Grzegorz Świrski 
Near semirings and lambda calculus by Rick Statman 

A connection between lambda calculus and the algebra of
near semirings is discussed. Among the results is the following completeness theorem. A firstorder equation in the language of binary associative distributive algebras is true in all such algebras if and only if the interpretations of
the first order terms as lambda terms betaeta convert to one another. A similar result holds for equations containing free variables. 
03.06.2015, Radosław Smyrek 
Best Response Analysis in Two Person Quantum Games by Azharuddin Shaik, Aden Ahmed 

In this paper, we find particular use for a maximally entangled initial state that produces a quantized
version of two player two strategy games. When applied to a variant of the wellknown game of Chicken, our construction shows the existence of new Nash equilibria with the players receiving better payoffs than those found in literature. 
27.05.2015, Bartłomiej Ryniec 
GENERIC COMPLEXITY OF UNDECIDABLE PROBLEMS by ALEXEI G. MYASNIKOV AND ALEXANDER N. RYBALOV 

In this paper we study generic complexity of undecidable problems. It turns out that some classical undecidable problems are, in fact, strongly undecidable, i.e., they
are undecidable on every strongly generic subset of inputs. For instance, the classical Halting Problem is strongly undecidable. Moreover, we prove an analog of the Rice’s
theorem for strongly undecidable problems, which provides plenty of examples of strongly undecidable problems. Then we show that there are natural superundecidable problems,
i.e., problem which are undecidable on every generic (not only strongly generic) subset of inputs. In particular, there are finitely presented semigroups with superundecidable word problem. To construct strongly and superundecidable problems we introduce a method of generic amplification (an analog of the amplification in complexity theory). Finally, we construct absolutely undecidable problems, which stay undecidable on every nonnegligible
set of inputs. Their construction rests on generic immune sets. 
13.05.2015, Bartosz Badura 
Havannah and TwixT are pspacecomplete by Édouard Bonnet, Florian Jamain, and Abdallah Saffidine 

Numerous popular abstract strategy games ranging from hex
and havannah to lines of action belong to the class of connection games. Still, very few complexity results on such games have been obtained since hex was proved pspacecomplete in the early eighties. We study the complexity of two connection games among the most widely played. Namely, we prove that havannah and twixt are pspacecomplete. The proof for havannah involves a reduction from generalized geography and is based solely on ringthreats to represent the input graph. On the other hand, the reduction for twixt builds up on previous work as it is a straightforward encoding of hex. 

references:

06.05.2015, Leszek Jakub Kania 
Fast algorithm finding the shortest reset words by A. Kisielewicz J. Kowalski, and M. Szykuła 

In this paper we present a new fast algorithm finding minimal reset words for finite synchronizing automata. The problem is know to be computationally hard, and our algorithm is exponential. Yet, it is faster than the algorithms used so far and it works well in practice. The main idea is to use a bidirectional BFS and radix (Patricia) tries to store and compare resulted subsets. We give both theoretical and practical arguments showing that the branching factor is reduced efficiently. As a practical test we perform an experimental study of the length of the shortest reset word for random automata with n states and 2 input letters. We follow Skvorsov and Tipikin, who have performed such a study using a SAT solver and considering automata up to n = 100 states. With our algorithm we are able to consider much larger sample of automata with up to n = 300 states. In particular, we obtain a new more precise estimation of the expected length of the shortest reset word = 2.5 sqrt{n − 5}. 
29.04.2015, Marcin Kostrzewa 
A Short Note on Typeinhabitation: FormulaTrees vs. Game Semantics by S. Alves, S. Broda 

This short note compares two different methods for exploring typeinhabitation in the simply typed lambdacalculus, highlighting their similarities. 
22.04.2015, Agnieszka Łupińska 
The Converse principal Type Algorithm by Roger Hindley 

One chapter from the book Basic Simple Type Theory 
15.04.2015, Agnieszka Łupińska 
The principal Type Algorithm by Roger Hindley 

One chapter from the book Basic Simple Type Theory 
01.04.2015, Maciej Bendkowski 
Über Tautologien, in welchen keine Variable mehr als zweimal vorkommt von S. Jaśkowski 

CONTINUATION 
25.03.2015, CANCELLED 



18.03.2015, Agnieszka Łupińska 
The principal Type Algorithm by Roger Hindley 

One chapter from the book Basic Simple Type Theory 
11.03.2015, CANCELED 



04.03.2015, Maciej Bendkowski 
Über Tautologien, in welchen keine Variable mehr als zweimal vorkommt von S. Jaśkowski 

H. Thiele hat im Jahre 1960 das Problem gestellt, das implikative Teilsystem des Aussagenkalküls mit dem Axiomen B,C,K zu untersuchen. Hier wird für dieses System und für ein anderes, in dem das letzte Axiom durch ein schwächeres, nämlich I ersetzt wird, ein Entscheidungsverfahren angegeben. Die Methode beruht auf einer Untersuchung von gewissen allgemeinen Eigenschaften der Ausdrücke, in welchen keine Satzvariable mehr als zweimal vorkommt. Dabei wird eine dreiwertige Matrix benutzt.

28.01.2015, 21.01.2015, Radosław Smyrek 
Symmetry groups of boolean functions by Mariusz Grech, Andrzej Kisielewicz 

We prove that every abelian permutation group, but known exceptions, is the symmetry group of a boolean function. This solves the problem posed in the book by Clote and Kranakis. In fact, our result is proved for a larger class of permutation groups, namely, for all subgroups of direct sums of regular permutation groups. 
14.01.2015, Bartłomiej Ryniec 
Infinite time Turing machines with only one tape by Joel David Hamkins, Daniel Evan Seabold 

Infinite time Turing machines with only one tape are in many respects fully as powerful as their multitape cousins. In particular, the two models of machine give rise to the same class of decidable sets, the same degree structure and, at least for functions f:R → N, the same class of computable functions. Nevertheless, there are infinite time computable functions f:R→R that are not
onetape computable, and so the two models of infinitary computation are not equivalent. Surprisingly, the class of onetape computable functions is not closed under composition; but closing it under composition yields
the full class of all infinite time computable functions. Finally, every ordinal which is clockable by an infinite time Turing machine is clockable by a onetape machine, except certain isolated ordinals that end gaps in the clockable ordinale 
07.01.2015, Michał Seweryn 
A Formalisation of the MyhillNerode Theorem Based on Regular Expressions by Chunhan Wu, Xingyuan Zhang, Christian Urban 

There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory—the MyhillNerode Theorem—can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow. 
17.12.2014, Agnieszka Łupińska 
Relevant Logic and the Philosophy of Mathematics by Edwin Mares 

This paper sets out three programmes that attempt to use relevant logic as the basis for a philosophy of mathematics. Although these three programmes do not exhaust the possible approaches to mathematics through relevant logic, they are fairly representative of the current state of the field.
The three programmes are compared and their relative strengths and weaknesses set out. At the end of the paper I examine the consequences of adopting each programme for the realist debate about mathematical objects. 

references:

10.12.2014, Pierre Lescanne (l'École Normale Supérieure de Lyon) 
Boltzmann samplers 


03.12.2014, Agnieszka Łupińska 
General information in relevant logic by Edwin D. Mares 

There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward
to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory—the MyhillNerode Theorem—can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow. 
26.11.2014, Konrad Witaszczyk 
Problems of Proof compexity by Jan Krajicek, Stephen A. Cook and Robert A. Reckhow 

The ultimate goal of proof complexity is to show that there is no universal propositional proof system allowing for efficient proofs of all tautologies. This is equivalent to showing that the computational complexity class NP is not closed under the complementation. By the universality propositional proof systems subsume methods from other parts of mathematics used for proving the nonexistence statements. Because of this, even the partial results known at present (lower bounds for some specific proof systems) revealed interesting links of proof complexity to logic, algebra, combinatorics, computational complexity. We will explain some basic points of proof complexity and give few informal examples in order to motivate the main concepts and problems of proof complexity. 
19.11.2014, Bartosz Badura 
On the Complexity of TrickTaking Card Games by Edouard Bonnet, Florian Jamain, and Abdallah Saffidine 

Determining the complexity of perfect information
tricktaking card games is a long standing open problem.
This question is worth addressing not only because of the popularity of these games among human players, e.g., DOUBLE DUMMY BRIDGE, but also because of its practical importance as a building block in stateoftheart playing engines for CONTRACT BRIDGE, SKAT, HEARTS, and SPADES. We define a general class of perfect information twoplayer tricktaking card games dealing with arbitrary numbers of hands, suits, and suit lengths. We investigate the complexity of determining the winner in various fragments of this game class. Our main result is a proof of PSPACEcompleteness
for a fragment with bounded number of hands, through a reduction from Generalized Geography. Combining our results with W¨astlund’s tractability results gives further insight in the complexity landscape of tricktaking card games. 
05.11.2014, Bartłomiej Ryniec 
Social Networks with Competing Products by Krzysztof Apt and Evangelos Markakis 

We introduce a new threshold model of social networks, in which the nodes influenced by their neighbours can adopt one out of several alternatives. We characterize social networks for which adoption of a product by the whole network is possible (respectively necessary) and the ones for which a unique outcome is guaranteed. These characterizations directly yield polynomial time algorithms that allow us to determine whether a given social network satisfies one of the above properties. We also study algorithmic questions for networks without unique outcomes.
We show that the problem of determining whether a final network exists in which all nodes adopted some product is NPcomplete. In turn, we also resolve the complexity of the problems of determining whether a given node adopts some (respectively, a given) product in some (respectively, all)
network(s). Further, we show that the problem of computing the minimum possible spread of a product is NPhard to approximate with an approximation ratio better than W(n), in contrast to the maximum spread, which is efficiently
computable. Finally, we clarify that some of the above problems can be solved in polynomial time when there are only two products. 
29.10.2014, Maciej Bendkowski 
INFINITE TIME TURING MACHINES AND AN APPLICATION TO THE HIERARCHY OF EQUIVALENCE RELATIONS ON THE REALS by SAMUEL COSKEY AND JOEL DAVID HAMKINS 

We describe the basic theory of infinite time Turing machines and some recent developments, including the infinite time degree theory, infinite time complexity theory, and infinite time computable model theory. We focus particularly on the application of infinite time Turing machines to the analysis of the hierarchy of equivalence relations on the reals, in analogy with the theory arising from Borel reducibility. We define a notion of infinite time reducibility, which lifts much of the Borel theory into the class $Delta^1_2$ in a
satisfying way. 
22.10.2014, Łukasz Lachowski 
Typed combinatory logic by Henk Barendregt 

Basic properties of typed combinatory logic 
15.10.2014, Łukasz Lachowski 
Combinatrory Logic by Henk Barendregt 

Basic properties of combinatory logic 
08.10.2014, Łukasz Lachowski 
Combinatrory Logic by Henk Barendregt 

Basic properties of combinatory logic 
11.06.2014, Gabriel Fortin 
"The safe lambda calculus" by William Blum and C.H. Luke Ong. 

Safety is a syntactic condition of higherorder grammars that constrains occurrences of variables in the production rules according to their typetheoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simplytyped lambda calculus. In contrast to the original deﬁnition of safety, our calculus does not constrain types (to be homogeneous). We show that in the safe lambda calculus, there is no need to rename bound variables when performing substitution, as variable capture is guaranteed not to happen. We also propose an adequate notion of βreduction that preserves safety. In the same vein as Schwichtenberg’s 1976 characterization of the simplytyped lambda calculus, we show that the numeric functions representable in the safe lambda calculus are exactly the multivariate polynomials; thus conditional is not deﬁnable. We also give a characterization of representable word functions. We then study the complexity of deciding betaeta equality of two safe simplytyped terms and show that this problem is PSPACEhard. Finally we give a gamesemantic analysis of safety: We show that safe terms are denoted by Pincrementally justiﬁed strategies. Consequently pointers in the game semantics of safe λterms are only necessary from order 4 onwards.

04.06.2014, Maciej Bendkowski 
On the shortest combinatory logic term without weak normalisation. 

Combinatory logic is a formal notation for function abstraction, eliminating the notion of bound variables. In our presentation, we give proofs of nonnormalization for two different Sterms, i.e. combinatory logic terms consisting of only one combinator S and term application, and present a computerassisted proof of the least combinatory logic term without normal form. We will then discuss the decidability of normalization in the set of Sterms.

28.05.2014, Radosław Smyrek 
A hierarchy of hereditarily finite sets by Laurence Kirby 

This article defines a hierarchy on the hereditarily finite sets which reflects the way sets are built up from the empty set by repeated adjunction, the addition to an already existing set of a single new element drawn from the already existing sets. The structure of the lowest levels of this hierarchy is examined, and some results are
obtained about the cardinalities of levels of the hierarchy. 
21.05.2014, Konrad Witaszczyk 
On the classification of recursive languages by John Case, Efim Kinber, Arun Sharma, and Frank Stephanc. 

A onesided classifier for a given class of languages converges to 1 on every language from the class and
outputs 0 infinitely often on languages outside the class. A twosided classifier, on the other hand, converges
to 1 on languages from the class and converges to 0 on languages outside the class. The present paper investigates
onesided and twosided classification for classes of recursive languages. Theorems are presented that
help assess the classifiability of natural classes. The relationships of classification to inductive learning theory
and to structural complexity theory in terms of Turing degrees are studied. Furthermore, the special case of
classification from only positive data is also investigated. 
14.05.2014, Patryk Zaryjewski 
ON THE AVERAGE STATE COMPLEXITY OF PARTIAL DERIVATIVE AUTOMATA: AN ANALYTIC COMBINATORICS APPROACH by SABINE BRODA, ANTONIO MACHIAVELO, NELMA MOREIRA and ROGERIO REIS 

The partial derivative automaton is usually smaller than other nondeterministic finite automata constructed from a regular expression, and it can be seen as a quotient
of the Glushkov automaton. By estimating the number of regular expressions that have \epsilon as a partial derivative, we compute a lower bound of the average number
of mergings of states in A_pos and describe its asymptotic behaviour. This depends on the alphabet size, k, and for growing k’s its limit approaches half the number of states
in Apos. The lower bound corresponds to consider the A_pd automaton for the marked version of the regular expression, i.e. where all its letters are made different. Experimental
results suggest that the average number of states of this automaton, and of the A_pd automaton for the unmarked regular expression, are very close to each other. 
07.05.2014, Maciej Gawron 
Constructions of asymptotically shortest kradius sequences by Jaromczyk, Zbigniew Lonc, Mirosław Truszczynski 

Let k be a positive integer. A sequence s over an nelement
alphabet A is called a kradius sequence if every two symbols from A occur in s at distance of at most k. Let f_k(n) denote the length of a shortest kradius sequence over A. We provide constructions demonstrating that
(1) for every fixed k and for every fixed ε > 0,
f_k(n) = 1 / 2k n^2 + O(n^{1+ε}) and
(2) for every k = n^α, where α is a fixed real such that 0 < α < 1, f_k(n) = 1/2k n^2 + O(n^β ), for some β < 2 − α. Since fk(n) 1/2k n^2 − n/2k , the constructions give
asymptotically optimal kradius sequences. Finally,
(3) we construct optimal 2radius sequences for a 2pelement alphabet, where p is a prime.

30.04.2014, Bartłomiej Ryniec 
Multiparty communication complexity and very hard functions by Pavol Duriš 

A boolean function f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i is hard if its nondeterministic multiparty communication complexity (introduced in [in: Proceedings of the 30th IEEE FOCS, 1989, p. 428–433]), C(f),
is at least nm. Note that C(f) n*m for each f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i. A boolean function
is very hard if it is hard and its complementary function is also hard. In this paper, we show that randomly chosen boolean function f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i is very hard with very high probability (for n 3 and m large enough). In [in: Proceedings of the 12th Symposium on Theoretical Aspects of Computer Science, LNCS 900, 1995, p. 350–360], it has been shown that if
f(x_1, . . . , x_k , . . . , x_n) =
f_1 (x_1, . . . , x_k ) · f_2(x_{k+1}, . . . , x_n), where C(f_1) > 0 and C(f_2) > 0, then C(f) = C(f1) + C(f2).We prove here an analogical result: If f(x_1, . . . , x_k , . . . , x_n) = f_1(x_1, . . . , x_k ) ⊕ f_2(x_{k+1}, . . . , x_n) then DC(f) = DC(f1) + DC(f2), where DC(g) denotes the deterministic multiparty communication complexity of the function g and “⊕” denotes the parity function.

23.04.2014, Maciej Gazda Eindhoven University of Technology 
Zielonka's Recursive Algorithm for Parity Games 

Parity games are infinite duration, two player games played on a finite directed graph. Vertices of the graph are labelled with natural numbers (called priorities) and the winning condition is determined by the parity of the most significant (typically maximal) priority encountered inifnitely often. The games are memoryless determined, moreover, the problem of finding the winning partition of a given game belongs to both NP and coNP complexity classes. On the other hand, no polynomial algorithm solving parity games has been found (the best one due to Jurdziński, Paterson and Zwick has subexponential running time with sqrt(n) in the exponent).
In my talk, I will give a brief introduction to this intriguing computational problem, and then focus on one of the earliest and simplest solving algorithms, namely Zielonka's recursive algorithm. Even though its worstcase running time is not particularly impressive as compared to more sophisticated solvers, the experimental study of Friedmann and Lange has shown that in practice it works very well. In order to understand why it is the case, in our recent work with Tim Willemse we have analysed the performance of two variants of the algorithm (standard and optimised) on certain subclasses of parity games (dull, weak, and solitaire). Moreover, we have provided a tighter lower bound on its worstcase running time. 
16.04.2014, Agnieszka Łupińska 
Efficient Bracket Abstraction Using Iconic Representations for Combinators by Antoni Diller 

Some fundamental properties of a new univariate bracket abstraction algorithm employing a string representation for combinators are established. In particular, if the input term has length n, where n > 1, the algorithm is called fewer than n times to produce the abstract. Furthermore, the space required to store the abstract, in the worst case, is of the order O(n). This algorithm also has a number of features that make it worthy of further attention. When it is used to abstract a variables from an input term of length n, where n > 1, fewer than an new combinators are introduced into the abstract. However, the
total size of the string representations of these combinators grows quadratically in the number of variables abstracted and the space required to store the abstract, in the worst case, is of the order O(a^2 n). Fortunately, a closely related singlesweep, multivariate algorithm
exists, using an array representation for combinators, which produces an abstract whose storage requirement, in the worst case, is of the order O(an). 
09.04.2014, Aleksandra Piktus 
Improved constructions of quantum automata by Andris Ambainis, Nikolajs Nahimovs 

We present a simple construction of quantum automata which achieve an exponential advantage over classical finite automata. Our automata use 4/epsion log (2p) states to recognize a language that requires p states classically. The construction is both substantially simpler and achieves a better constant in the front of log p than the previously known construction. Our construction is by a probabilistic argument. We consider the possibility to derandomize it and present some results in this direction. 
02.04.2014, Łukasz Janiszewski 
Exploiting independent subformulas: A faster approximation scheme for #kSAT by Manuel Schmitt , Rolf Wanka 

We present an improvement on Thurley’s recent randomized approximation scheme for #kSAT where the task is to count the number of satisfying truth assignments of a Boolean function Φ given as an nvariable kCNF. We introduce a novel way to identify independent substructures of Φ and can therefore reduce the size of the search space considerably. Our randomized algorithm works for any k. For #3SAT, it runs in time O(ε−2 · 1.51426n), for #4SAT, it runs in time O(ε−2 · 1.60816n), with error bound ε. 
26.03.2014, Michał Marczyk 
CAP theorem 

We will examine Gilbert and Lynch's proof of Brewer's conjecture. The latter states that it is impossible for a
distributed service to be simultaneously consistent, available and partitiontolerant (for certain natural definitions of these terms). We will then consider the realworld impact of the theorem. Based on Gilbert, Lynch, "Brewer's Conjecture and the Feasibility of Consistent, Available, PartitionTolerant Web Services". 
19.03.2014, Seminar cancelled 
DAY OF FACULTY OF MATHEMATICS AND COMPUTER SCIENCE 


12.03.2014, cancelled 



05.03.2014, Robert Obryk 
Cryptographic Accumulators 

A cryptographic accumulator is a less wellknown cousin of a
cryptographic hash function: it allows a digest of a multiset to be constructed one element at a time. One can also extend this notion in a few ways: allow removing elements already added to the digest, or provide witnesses that prove validity of operations on the digest without giving away what operations they were. This talk will present the basic notion of accumulators and their properties, give example implementations (secure under the typical assumptions) and hint at their possible uses.

26.02.2014, Adam Polak 
Open problems for pattern languages 

A pattern is a string built of terminals and variables. A language generated by a given pattern consists of words produced by substituting variables with arbitrary strings of terminals. Of course every occurrence of the same variable has to be substituted with the same string. Pattern languages were first studied in the context of machine learning but soon attracted formal languages researchers. Despite their very simple definition they have numerous interesting properties. During the seminar we will discuss several intriguing computational and structural problems involving pattern languages and their relation to the Chomsky hierarchy. Some of them were recently solved and some remain open.
Papers about pattern languages:
http://www.tks.informatik.unifrankfurt.de/data/doc/dissertation.pdf
http://link.springer.com/chapter/10.1007%2F3540569391_81
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3057&rep=rep1&type=pdf
http://www.sciencedirect.com/science/article/pii/S0890540109001023
http://www.tks.informatik.unifrankfurt.de/data/doc/dlt2010.pdf
http://www.comp.nus.edu.sg/~sanjay/paps/regpat.pdf
http://www.sciencedirect.com/science/article/pii/S030439751300577X

22.01.2014, Maciej Bendkowski 
An upper bound for reduction sequences in the typed lambdacalculus by H. Schwichtenberg 

It is well known that the full reduction tree for any term of the typed λ–calculus is finite. However, it is not obvious how a reasonable estimate for its height might be obtained. Here we note that the head reduction tree has the property tha the number of its nodes with conversions bounds the length of any reduction sequence. The height of
that tree, and hence also the number of its nodes, can be estimated using a technique due to Howard [3], which in turn is based on work of Sanchis [4] and Diller [1]. This
gives the desired upper bound. The method of Gandy [2] can also be used to obtain a bound for the length of
arbitrary reduction sequences; this is carried out in [5]. However, the bound derived here, apart from being more intelligible, is also better.

15.01.2014, Konrad Witaszczyk 
Analytic aspects of the shuffle product by Marni Mishna, Mike Zabrocki 

There exist very lucid explanations of the combinatorial origins of rational and algebraic functions, in particular with respect to regular and context free languages. In the
search to understand how to extend these natural correspondences, we find that the shuffle product models many key aspects of Dfinite generating functions, a class which contains algebraic. We consider several different takes on the shuffle product, shuffle closure, and shuffle grammars, and give explicit generating function consequences. In the process, we define a grammar class that models Dfinite generating functions. 
08.01.2014, Michał Bejda 
Generalized satisfability problems: minimal elements and phase transitions by Nadia Creignoua, Herve Daud 

We develop a probabilistic model on the generalized satisfability problems defned by Schaefer (in: Proceedings of the 10th STOC, San Diego, CA, USA, Association for Computing Machinery, New York, 1978, pp. 216–226) for which the arity of the constraints is fixed in order to study
the associated phase transition. We establish new results on minimal elements associated with such generalized satis"ability problems. These results are the keys of the exploration we conduct on the location and on the nature of the phase transition for generalized satisfability. We first
prove that the phase transition occurs at the same scale for every reasonable problem and we provide lower and upper bounds for the associated critical ratio. Our framework allows one to get these bounds in a uniform way, in particular, we obtain a lower bound proportional to the
number of variables for kSAT without analyzing any algorithm. Finally, we reveal the seed of coarseness for the phase transition of generalized satisfability: 2XORSAT. 

references:

18.12.2013, Łukasz Janiszewski 
. Exploiting independent subformulas: A faster approximation scheme for #kSAT by Manuel Schmitt , Rolf Wanka 

We present an improvement on Thurley’s recent randomized approximation scheme for #kSAT where the task is to count the number of satisfying truth assignments of a Boolean
function Φ given as an nvariable kCNF. We introduce a novel way to identify independent substructures of Φ and can therefore reduce the size of the search space considerably. Our randomized algorithm works for any k. For #3SAT, it runs in time O(ε−2 · 1.51426n), for #4SAT, it runs in time O(ε−2 · 1.60816n), with error bound ε. 
11.12.2013, Michał Dyrek 
Boundary properties of the satisfiability problems by Vadim Lozin , Christopher Purcell 

The satisfiability problem is known to be NPcomplete in general and for many restricted instances, such as CNF formulas with at most 3 variables per clause and at most
3 occurrences per variable, or planar formulas. The latter example refers to graphs representing satisfiability instances. These are bipartite graphs with vertices representing clauses and variables, and edges connecting variables to the clauses containing them. Finding the strongest possible restrictions under which the problem remains NPcomplete is important for at least two reasons. First, this can make it easier to establish the NP completeness of new problems by allowing easier transformations. Second, this can help clarify the boundary between tractable and intractable instances of the problem. In this paper, we address the second issue and reveal the first boundary property of graphs representing satisfiability instances. 
04.12.2013, Przemysław Jedynak 
A MyhillNerode theorem for automata with advice by Alex Kruckman, Sasha Rubin, John Sheridan 

An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the MyhillNerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice. 
27.11.2013, Adam Polak 
On the satisfiability threshold and clustering of solutions of random 3SAT formulas, by Elitza Maneva, Alistair Sinclair 

We study the structure of satisfying assignments of a random 3Sat formula. In particular, we show that a random formula of density 4:453 almost surely has no nontrivial
``core'' assignments. Core assignments are certain partial assignments that can be extended to satisfying assignments, and have been studied recently in connection with the Survey
Propagation heuristic for random Sat. Their existence implies the presence of clusters of solutions, and they have been shown to exist with high probability below the satisfiability threshold for kSat with k 9 [D. Achlioptas, F. RicciTersenghi, On the solutionspace
geometry of random constraint satisfaction problems, in: Proc. 38th ACM Symp. Theory of Computing, STOC, 2006, pp. 130139]. Our result implies that either this does not hold
for 3Sat, or the threshold density for satisfiability in 3Sat lies below 4.453. The main technical tool that we use is a novel simple application of the first moment method. 
20.11.2013, Andrzej Dorobisz 
Regular Languages Accepted by Quantum Automata by Alberto Bertoni and Marco Carpentieri 

In this paper we analyze some features of the behaviour of quantum automata. In particular we prove that the class of languages recognized by quantum automata with isolated cut point is the class of reversible regular languages. As a more general result, we give a bound on the inverse error that
implies the regularity of the language accepted by a quantum automaton 
13.11.2013, Kamil Jarosz 
On the strongly generic undecidability of the Halting Problem by Alexander Rybalov 

It has been shown in [J.D. Hamkins, A. Miasnikov, The halting problem is decidable on a set of asymptotic probability one, Notre Dame J. Formal Logic 47(4) (2006) 515–524] that the classical Halting Problem for Turing machines with oneway tape is decidable on a “large” set of Turing machines (a socalled generic set). However, here we prove that the Halting Problem remains undecidable when restricted to an arbitrary “very large” set of Turing machines (a socalled strongly generic set). Our proof is
independent of a Turing machine model.

06.11.2013, Michał Masłowski 
The Halting Problem Is Decidable on a Set of Asymptotic Probability One by Joel David Hamkins and Alexei Miasnikov 

The halting problem for Turing machines is decidable on a set of asymptotic probability one. The proof is sensitive to the particular computational models.

30.10.2013, Agnieszka Łupińska 
Design and Implementation of a Parallel Priority Queue on Manycore Architectures by Xi He, Dinesh Agarwal, and Sushil K. Prasad 

An efficient parallel priority queue is at the core
of the effort in parallelizing important nonnumeric irregular computations such as discrete event simulation scheduling and branchandbound algorithms. GPGPUs can provide powerful computing platform for such nonnumeric computations if an efficient parallel priority queue implementation is available. In this paper, aiming at finegrained applications, we develop an efficient
parallel heap system employing CUDA. To our knowledge,
this is the first parallel priority queue implementation on manycore architectures, thus represents a breakthrough. By allowing wide heap nodes to enable thousands of simultaneous deletions of highest priority items and insertions of new items, and taking full advantage of CUDA’s data parallel SIMT architecture, we demonstrate up to 30fold absolute speedup for relatively finegrained
compute loads compared to optimized sequential priority
queue implementation on fast multicores. Compared to this, our optimized multicore parallelization of parallel heap yields only 23 fold speedup for such finegrained loads. This parallelization of a treebased data structure on GPGPUs provides a roadmap for future parallelizations of other such data structures.


references:

23.10.2013, Michał Marczyk 
Consistency in distributed systems, part II: avoiding synchronization with CRDTs (based on a paper by Shapiro, Preguiça, Baquero, Zawirski) 

In this closing part of a twopart series we will consider CRDTs, a systematic approach to eventual consistency. We will examine both the statebased and the operationbased approach, with some concrete examples. Finally, we will return to our motivating discussion from part I in considering how a system may incorporate both an eventually
consistent data store and a limited dose of consensus to achieve excellent functional guarantees in a distributed setting.
Key source: Shapiro, Preguiça, Baquero, Zawirski, "A comprehensive
study of Convergent and Commutative Replicated Data Types",
http://hal.inria.fr/inria00555588/

16.10.2013, Marek Markiewicz 
Cellular Automata on a Toeplitz Space. 

Toeplitz Space is a set of regular quasiperiodic biinfinite words over a finite alphabet with at least two different letters endowed with a Besicovitch metric. It is an invariant set for every Cellular Automaton. During the talk I will present some properties of this space and I will discuss how CA behave on it. I will also present an idea of examining the continuity of evolution of a CA and show some very basic results in this topic.


references:

13.10.2013,




09.10.2013, Michał Marczyk 
Consistency in distributed systems, part I: achieving consensus with Raft (presenting research by Ongaro & Ousterhout) 

In this opening part of a twopart series we will consider Raft, a new protocol for achieving consensus in a distributed system. Raft matches Paxos as far as efficiency is concerned, but is designed to be more readily understandable and more amenable to implementation without
tweaks and additional optimizations. To motivate the discussion, we will briefly consider the concept of a distributed system and the circumstances in which such systems may or may not require consensus
to make progress safely.
Key source: Ongaro, Ousterhout, "In Search of an Understandable Consensus Algorithm" (draft, 20130910),
https://ramcloud.stanford.edu/wiki/download/attachments/11370504/raft.pdf 
05.06.2013, Łukasz Janiszewski 
Tetris is Hard, Even to Approximate by Erik D. Demaine, Susan Hohenberger and David LibenNowell 

In the popular computer game of Tetris, the player is given a sequence of tetromino pieces and must pack them into a rectangular gameboard initially occupied by a given configuration of filled squares; any completely filled row of the gameboard is cleared and all pieces above it drop
by one row. We prove that in the offline version of Tetris, it is NPcomplete to maximize the number of cleared rows, maximize the number of tetrises (quadruples of rows simultaneously filled and cleared), minimize the maximum height of an occupied square, or maximize the number
of pieces placed before the game ends. We furthermore show the extreme inapproximability of the first and last of these objectives to within a factor of p^{1−epsilon}, when given a sequence of p pieces, and the inapproximability of the third objective to within a factor of 2−epsilon, for any epsilon>0. Our results hold under several variations on the rules of Tetris, including different models of rotation, limitations on player agility, and restricted piece sets. 
22.05.2013, Aleksandra Piktus 
On the Additive Constant of the kServer Work Function Algorithm' by Yuval Emek, Pierre Fraigniaud, Amos Korman i Adi Rosen 

We consider the Work Function Algorithm for the kserver problem (Chrobak andr Larmore, 1991; Koutsoupias and Papadimitriou, 1995). We show that if the Work Function Algorithm is ccompetitive, then it is also strictly (2c)competitive. As a consequence of (Koutsoupias and
Papadimitriou, 1995) this also shows that the Work Function Algorithm is strictly (4k2)competitive.

15.05.2013, Dawid Pustułka 
An alternate proof of Statman’s finite completeness theorem by B. Srivathsan, Igor Walukiewicz 

Statman’s finite completeness theorem says that for every pair of nonequivalent terms of simplytyped lambdacalculus there is a model that separates them. A direct method of
constructing such a model is provided using a simple induction on the Böhm tree of the term. 
08.05.2013, Aneta Pawłowska 
TETRAVEX is NPcomplete by Yasuhiko Takenaga and Toby Walsh 

Tetravex is a widely played one person computer game in which you are given n^2 unit tiles, each edge of which is labelled with a number. The objective is to place each tile within a n by n square such that all neighbouring edges are
labelled with an identical number. Unfortunately, playing Tetravex is computationally hard. More precisely, we prove that deciding if there is a tiling of the Tetravex board given n^2 unit tiles is NPcomplete. Deciding where to place
the tiles is therefore NPhard. This may help to explain why Tetravex is a good puzzle. This result compliments a number of similar results for one person games involving tiling. For example, NPcompleteness results have been show
for: the offline version of Tetris, KPlumber (which involves rotating tiles containing drawings of pipes to make a connected network), and shortest sliding puzzle problems. It raises a number of open questions. For example, is the infinite version Turingcomplete? How do we generate Tetravex problems which are truly puzzling as random NPcomplete problems are often surprising easy to solve? Can we observe phase transition behaviour?
What about the complexity of the problem when it is guaranteed to have an unique solution? How do we generate puzzles with unique solutions? 
24.04.2013, Maria Chmaj 
Weight automata 


17.04.2013, Monika Krupnik 
Inclusion problems for patterns with a bounded number of variables by Joachim Bremer, Dominik D. Freydenberger 

We study the inclusion problems for pattern languages that are generated by patterns with a bounded number of variables. This continues the work by Freydenberger
and Reidenbach (Information and Computation 208 (2010)) by showing that restricting the inclusion problem to significantly more restricted classes of patterns preserves undecidability, at least for comparatively large bounds.
For smaller bounds, we prove the existence of classes of patterns with complicated inclusion relations, and an open inclusion problem, that are related to the Collatz Conjecture. In addition to this, we give the first proof of the undecidability of the inclusion problem for NEpattern languages that, in contrast to previous proofs, does not rely on the inclusion problem for Epattern languages,
and proves the undecidability of the inclusion problem for NEpattern languages over binary and ternary alphabets. 
10.04.2013, Borg Łojasiewicz 
The state complexities of some basic operations on regular languages by Sheng Yu, Qingyu Zhuang and Kai Salomaa 

We consider the state complexities of some basic operations on regular languages. We show that the number of states that is sufficient and necessary in the worst case for a deterministic finite automaton DFA) to accept the catenation of an mstate DFA language and an nstate DFA language is exactly m2^n  2^{n1} for m,n> 1. The result of 2^{n1}+2^{n2} states is obtained for the star of an nstate DFA language, n>1. State complexities for other basic operations and for regular languages over a oneletter alphabet are also studied. 

references:

03.04.2013, Michał Bejda 
Subshifts, Languages and Logic by Emmanuel Jeandel and Guillaume Theyssier 

We study the Monadic Second Order (MSO) Hierarchy over
infinite pictures, that is tilings. We give a characterization of existential MSO in terms of tilings and projections of tilings. Conversely, we characterise
logic fragments corresponding to various classes of infinite pictures (subshifts of finite type, sofic subshifts). 
27.03.2013, Jacek Szmigiel 
Bad news on decision problems for patterns by Dominik D. Freydenberger, Daniel Reidenbach 

We study the inclusion problem for pattern languages, which—due to Jiang et al. [T. Jiang, A. Salomaa, K. Salomaa, S. Yu, Decision problems for patterns, Journal of Computer and System Sciences 50 (1995) 53–63]— is known to be undecidable. More precisely, Jiang et al. demonstrate that there is no effective procedure deciding the inclusion for the class of all pattern languages over all alphabets. Most applications of pattern languages, however, consider classes over fixed alphabets, and therefore it is practically more relevant to ask for the existence of alphabetspecific decision procedures. Our first main result states that, for all but very particular cases, this version of the inclusion problem is also undecidable.
The second main part of our paper disproves the prevalent conjecture on the inclusion of socalled similar Epattern languages, and it explains the devastating consequences of this result for the intensive previous research on the most prominent open decision problem for pattern languages, namely the equivalence problem for general Epattern languages. 
20.03.2013,

Cancelled  DAY OF SCHOOL OF MATHEMATICS AND COMPUTER SCIENCE 


13.03.2013, Marek Markiewicz 
Topology on words 

During the talk we will explore two types of topologies on the set of all infinite words over a finite alphabet with at least two different letters: the Cantor topology and its relative version U^\delta topology for an arbitrary languge U of finite words. We will describe close and open sets in both topologies and how they relate to each other. We will also explore the definitions of Chaitin and MartinLöf random sequences and will prove their equivalence. Finally we will show that the set of MartinLöf random sequences is conowhere dense in U^\delta topology for a special U. The talk is based on three papers: Topological characterization of random sequences by C. Calude, S. Marcus, L. Steiger; Weighted Finite Automata and Mertics in Cantor Space by L. Steiger and Exploring Randomness by G. Chaitin. 
27.02.2013, Marek Markiewicz 
Topology on words 


23.01.2013, Adam Polak 
On the Complexity of the Equivalence Problem for Probabilistic Automata by Stefan Kiefer, Andrzej S. Murawski, Jo¨el Ouaknine, Bj¨orn Wachter1, and James Worrell 

Checking two probabilistic automata for equivalence has
been shown to be a key problem for efficiently establishing various behavioural and anonymity properties of probabilistic systems. In recent experiments a randomised equivalence test based on polynomial identity testing outperformed deterministic algorithms. In this paper we show
that polynomial identity testing yields efficient algorithms for various generalisations of the equivalence problem. First, we provide a randomized NC procedure that also outputs a counterexample trace in case of inequivalence. Second, we show how to check for equivalence two probabilistic automata with (cumulative) rewards. Our algorithm runs in deterministic polynomial time, if the number of reward counters is fixed. Finally we show that the equivalence problem for probabilistic
visibly pushdown automata is logspace equivalent to the Arithmetic Circuit Identity Testing problem, which is to decide whether a polynomial represented by an arithmetic circuit is identically zero. 
16.01.2013, Paweł Wanat 
The Local Lemma is Tight for SAT by H. Gebauer 

We construct unsatisfiable kCNF formulas where every
clause has k distinct literals and every variable appears in
at most (2/e + o(1))2^k/k clauses. The lopsided Local Lemma shows that our result is asymptotically best possible: every kCNF formula where every variable appears in at most 2^(k+1)/e(k+1) 1 clauses is satisfiable. The determination of this extremal function is particularly important as it represents the value where the kSAT problem exhibits its complexity hardness jump: from having every instance being a YESinstance it becomes NPhard just by allowing each variable to occur in one more clause. The asymptotics of other related extremal functions are also determined. Let l(k) denote the maximum number, such that every kCNF formula with each clause containing k distinct literals and each clause having a common variable with at most l(k) other clauses, is satisfiable. We establish that the bound on l(k) obtained from the Local Lemma is asymptotically optimal, i.e., l(k) = (1/e + o(1))2^k.
The constructed formulas are all in the class MU(1) of
minimal unsatisfiable formulas having one more clause than
variables and thus they resolve these asymptotic questions
within that class as well. 

references:

09.01.2013, Andrzej Dorobisz 
Functions definable by numerical setexpressions by IAN PRATTHARTMANN and IVO DÜNTSCH 

A numerical setexpression is a term specifying a cascade of arithmetic and logical operations to be performed on sets of nonnegative integers. If these operations are confined to the usual Boolean operations together with the result of lifting addition to the level of sets, we speak of additive circuits. If they are confined to the usual Boolean operations together with the result of lifting addition and multiplication to the level of sets, we speak of arithmetic circuits. In this article, we investigate the definability of sets and functions by means of additive and arithmetic circuits, occasionally augmented with additional operations. 

references:

19.12.2012, Przemysław Jedynak 
SUBWORD OCCURRENCES, PARIKH MATRICES AND LYNDON IMAGES by ARTO SALOMAA and SHENG YU 

We investigate the number of occurrences of a word u as a (scattered) subword of a word w. The notion of a Parikh matrix, recently introduced, is a basic tool in this investigation. In general, several words are associated with a Parikh matrix. The ambiguity can be resolved by associating a unique word called the Lyndon image to each Parikh matrix. In this paper we will investigate properties of Lyndon images and the corresponding questions of ambiguity. We give an exhaustive characterization in the case of a binary alphabet. Our main results in the general case deal with the comparison of unambiguous words and Lyndon images, algorithms for constructing Lyndon images, as well as classes of words with the same Parikh matrix, obtained by circular variance. 
12.12.2012, Maciej Bendkowski 
NONDETERMINISTIC FINITE AUTOMATA RECENT RESULTS ON THE DESCRIPTIONAL AND COMPUTATIONAL COMPLEXITY by MARKUS HOLZER and MARTIN KUTRIB 

continuation 
05.12.2012, Maciej Bendkowski 
NONDETERMINISTIC FINITE AUTOMATA RECENT RESULTS ON THE DESCRIPTIONAL AND COMPUTATIONAL COMPLEXITY by MARKUS HOLZER and MARTIN KUTRIB 

Nondeterministic finite automata (NFAs) were introduced in [68], where their equivalence to deterministic finite automata was shown. Over the last 50 years, a vast literature documenting the importance of finite automata as an enormously valuable concept has been developed. In the present paper, we tour a fragment of this literature. Mostly, we discuss recent developments relevant to NFAs related problems like, for example,
(i) simulation of and by several types of finite automata, (ii) minimization and approximation,
(iii) size estimation of minimal NFAs, and
(iv) state complexity of language operations.
We thus come across descriptional and computational complexity issues of nondeterministic finite automata. We do not prove these results but we merely draw attention to the big picture and some of the main ideas involved. 
28.11.2012, Maciej Gawron 
Hilbert's tenth problem 

The question of finding an algorithm to determine whether a given Diophantine equation has an integer solution, was one of the famous Hilbert's problems, posed in 1900. It was finally answered (negatively) by Yuri Matiyasevich in 1970. We will
show the proof of this fact. We will introduce the notion of Diophantine sets, relations and functions. We will prove that Diophantine sets are exactly computably enumerable sets. We will show that there exists an universal Diophantine equation, then using standard diagonal method we will prove that Hilbert's tenth problem is undecidable.

21.11.2012, Arkadiusz Olek 
Verifiable secret sharing in a total of three rounds by Shashank Agrawal 

Verifiable secret sharing (VSS) is an important building block in the design of secure multiparty protocols, when some of the parties are under the control of a malicious adversary. Henceforth, its round complexity has been the subject of intense study. The best known unconditionally secure protocol takes 3 rounds in sharing phase, which is known to be optimal, and 1 round in reconstruction. Recently, by introducing a negligible probability of
error in the definition of VSS, Patra et al. [CRYPTO 2009] have designed a novel protocol which takes only 2 rounds in sharing phase. However, the drawback of their protocol is that it takes 2 rounds in reconstruction as well. Hence, the total number of rounds required for VSS remains the same. In this paper, we present a VSS protocol which takes a total of 3 rounds only—2 rounds in
sharing and 1 round in reconstruction. 
14.11.2012, Michał Marczyk 
Unification type of bounded distributive lattices 

We will present S. Ghilardi's proof of his unification type theorem for bounded distributive lattices. The focus will be on the main result; a highlevel overview of the underlying methodology will be presented without detailed proofs of the individual results (which have been discussed in this seminar at an earlier date). The theorem as well as the methodology employed in establishing it have been presented in S. Ghilardi, "Unification through Projectivity", Journal
of Logic and Computation (1997) 7. 
07.11.2012, Katarzyna Grygiel 
Finite lattices and their weighted double skeletons 

In 1973 Christian Herrmann introduced the notion of the skeleton of a finite lattice. The skeleton of a lattice, however, does not suffice to reconstruct the initial lattice uniquely. Even worse, it turns out that every finite lattice is the skeleton of infinitely many nonisomorphic distributive lattices. At this point a natural question arises whether one can stuff the skeleton with some additional data in order to restore the original lattice. During the talk I will focus on the socalled weighted double skeletons. These objects, not being lattices themselves, turn out to fully characterize a particular kind of lattices.

31.10.2012, Michał Sapalski 
The nonuniform Bounded Degree Minimum Diameter Spanning Tree problem with an application in P2P networking by Jakarin Chawachat, Jittat Fakcharoenphol, Wattana Jindaluang 

This paper considers the Bounded Degree Minimum Diameter Spanning Tree problem (BDST problem) with nonuniform degree bounds. In this problem, we are given a metric
length function over a set V of n nodes and a degree bound Bv for each v ∈ V, and want to find a spanning tree with minimum diameter such that each node v has degree at most Bv . We present a simple extension of an O(logn ) approximation algorithm for this problem with uniform degree bounds of Könemann, Levin, and Sinha [J. Könemann, A. Levin, A. Sinha, Approximating the degreebounded minimum diameter spanning tree problem, in: Algorithmica, Springer, 2003, pp. 109–121] to work with nonuniform
degree bounds. We also show that this problem has an application in the peerto peer content distribution. More specifically, the Minimum Delay Mesh problem (MDM
problem) introduced by Ren, Li and Chan [D. Ren, Y.T. Li, S.H. Chan, On reducing mesh delay for peertopeer live streaming, in: INFOCOM, 2008, pp. 1058–1066] under a natural
assumption can be reduced to this nonuniform case of the BDST problem. 
24.10.2012, Agnieszka Łupińska 
On building minimal automaton for subset matching queries by Kimmo Fredriksson 

We address the problem of building an index for a set D of n strings, where each string location is a subset of some finite integer alphabet of size σ, so that we can answer efficiently if a given simple query string (where each string location is a single symbol) p occurs in the set. That is, we need to efficiently find a string d ∈ D such that p[i] ∈ d[i] for every i. We show how to build such index in O(nlogσ/(σ) log(n)) average time, where
is the average size of the subsets. Our methods have applications e.g. in computational biology (haplotype inference) and music information retrieval. 
17.10.2012, Michał Masłowski 
Regular patterns, regular languages and contextfree languages by Sanjay Jain, Yuh Shin Ong, Frank Stephan 

In this paper we consider two questions. First we consider whether every pattern language which is regular can be generated by a regular pattern. We show that this is indeed the case for extended (erasing) pattern languages if alphabet size is at least four. In all other cases, we show that there are patterns generating a regular language which cannot be generated by a regular pattern. Next we consider whether there are pattern languages which are contextfree but not regular. We show that, for alphabet size 2 and 3, there are both erasing and nonerasing pattern languages which are contextfree but not regular. On the other hand, for alphabet size at least 4, every erasing pattern language which is contextfree is also regular. It is open at present whether there exist nonerasing pattern languages which are contextfree but not regular for alphabet size at least 4. 
10.10.2012, Piotr Wójcik 
Some results about decidability of sets of tautologies in first order languages. 

The fundamental question whether a set of first order tautologies is decidable was answered (negatively) by Church in 1936. By restricting the classes of considered sentences (e.g. by reducing the number of function symbols or the arity of predicates), we can produce some positive results. After exploring wellknown languages, we will move on to study more complex systems, like first order monadic temporal logic. There, even without function symbols and equality, the set of tautologies is not recursively enumerable. 
03.10.2012, Mateusz Kostanek 
Reconciliation of elementary order and metric fixpoint theorems 

We prove two new fixed point theorems for generalized metric spaces and show that various fundamental fixed point principles, including: Banach Contraction Principle, Caristi fixed point theorem for metric spaces, KnasterTarski fixed point theorem for complete lattices, and the BourbakiWitt fixed point theorem for directedcomplete orders, follow as corollaries of our results. 
13.06.2012, Michał Marczyk 
Persistent data structures 

Persistent data structures, that is data structures which are immutable and support efficient creation of slightly modified copies with no change to the complexity guarantees of the basic operations (both on the copy and on the original) are of key importance for the performance of programs written in the functional paradigm. We will
examine in some detail a single example, namely a hash table offering logarithmic complexity of the basic operations with very good constants. The data structure in question is based on the mutable Hash Array Mapped Trie described in Phil Bagwell's paper "Ideal Hash Trees"
[1] (see also Phil Bagwell, "Fast And Space Efficient Trie Searches" [2]). The persistent version was pioneered by Rich Hickey and is used in the Clojure programming language [3], [4], [5] ([4]  the Java implementation used in Clojure; [5]  the ClojureScript port of [4] used in ClojureScript).
[1] http://lampwww.epfl.ch/papers/idealhashtrees.pdf
[2] http://lampwww.epfl.ch/papers/triesearches.pdf.gz
[3] http://clojure.org/
[4] https://github.com/clojure/clojure/blob/0ba3ff1a059625704500445c2d8553811301520b/src/jvm/clojure/lang/PersistentHashMap.java
[5] https://github.com/clojure/clojurescript/blob/fd1988c17a6b48115287de7805c4753d1fd5ef33/src/cljs/cljs/core.cljs#L3538


references:

06.06.2012, Michał Handzlik 
Asymetric grammars 

Asymetric gramars are natural generalization of leftist grammars.
Leftist grammars were introduced by Motwani as a tool useful to study accessibility problems in some protection systems. Since then, some interesting languagetheoretical research has been carried out in this field. For example, the membership problem for leftist grammar is decidable.
We propose a natural way to generalize the notion od leftist grammar. We study how this generalization affects the location of languages generated by those grammars within the Chomsky hierarchy. The main result states that membership problem for asymetric grammars is undecidable. 
30.05.2012, Marek Markiewicz 
A new class of hyperbent Boolean functions in binomial forms by Baocheng Wang, Chunming Tang, Yanfeng Qi, Yixian Yang and Maozhi Xu 

Bent functions, which are maximally nonlinear Boolean functions with even numbers of variables and whose Hamming distance to the set of all affine functions equals
2^{n−1} ± 2^{n/2 −1}, were introduced by Rothaus in 1976
when he considered problems in combinatorics. Bent unctions have been extensively studied due to their applications in cryptography, such as Sbox, block cipher and stream cipher. Further, they have been applied to coding theory, spread spectrum and combinatorial design. Hyperbent functions, as a special class of bent functions, were introduced by Youssef and Gong in 2001, which have stronger properties and rarer elements. Many research focus on the construction of bent and hyperbent functions. 
23.05.2012, Maciej Bendkowski 
On the expressive power of schemes by Dowek G, Jiang Y 

We present a calculus, called the schemecalculus, that permits to express natural deduction proofs in various theories. Unlike lambdacalculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its nondeterminism, some typed schemecalculi have the same expressivity as the corresponding typed lambdacalculi. 
09.05.2012, Piotr Zaborski 
APPROXIMATION ALGORITHMS FOR THE EUCLIDEAN TRAVELING SALESMAN PROBLEM WITH DISCRETE AND CONTINUOUS NEIGHBORHOODS by KHALED ELBASSIONI, ALEKSEI V. FISHKIN and RENE SITTERS 

In the Euclidean traveling salesman problem with discrete neighborhoods, we are given a set of points P in the plane and a set of n connected regions (neighborhoods), each
containing at least one point of P. We seek to nd a tour of minimum length which visits at least one point in each region. We give
(i) an O(\alpha)approximation algorithm for the
case when the regions are disjoint and fat, with possibly varying size;
(ii) an O(\alpha^3) approximation algorithm for intersecting fat regions with comparable diameters. These
results also apply to the case with continuous neighborhoods, where the sought TSP tour can hit each region at any point. We also give (iii) a simple O(logn)approximation algorithm for continuous nonfat neighborhoods. The most distinguishing features of these algorithms are their simplicity and low runningtime complexities. 
25.04.2012, Maciej Gawron 
COUNTING dDIMENSIONAL POLYCUBES AND NONRECTANGULAR PLANAR POLYOMINOES by GADI ALEKSANDROWICZ and GILL BAREQUET 

A planar polyomino of size n is an edgeconnected set of n squares on a rectangular twodimensional lattice. Similarly, a ddimensional polycube (for d 2) of size n is
a connected set of n hypercubes on an orthogonal ddimensional lattice, where two hypercubes are neighbors if they share a (d1)dimensional face. There are also twodimensional polyominoes that lie on a triangular or hexagonal lattice. In this paper we describe a generalization of Redelmeier's algorithm for counting twodimensional rectangular polyominoes, which counts all the above types of polyominoes. For example, our program computed the number of distinct threedimensional polycubes of size 18. To the best of our knowledge, this is the first tabulation of this value. 
18.04.2012, Patryk Zaryjewski 
Deciding if a Regular Language is Generated by a Splicing System by Lila Kari Steffen Kopecki 

Splicing as a binary word/language operation is inspired by the DNA recombination under the action of restriction enzymes and ligases, and was first introduced by Tom Head in 1987. Shortly after, it was proven that the languages generated by (finite) splicing systems form a proper subclass of the class of regular languages. However, the question of whether or not one can decide if a given regular language is generated by a splicing system remained open. In this paper we give a positive answer to this question. We namely prove that if a language is generated by a splicing system, then it is also generated by a splicing system whose size is a function of the size of the syntactic monoid of the input language, and which can be
effectively constructed. 
04.04.2012, Michał Feret 
Optimal Stopping and Applications 5 

Chapter 6. Maximizing the Rate of Return. 

references: Thomas S. Ferguson, Optimal Stopping and Applications

28.03.2012, Agnieszka Łupińska 
Optimal Stopping and Applications 4 

Chapter 5. Monotone Stopping Rule Problems. 

references: Thomas S. Ferguson, Optimal Stopping and Applications

21.03.2012, Szymon Kałasz 
Optimal Stopping and Applications 3 

Chapter 3. THE EXISTENCE OF OPTIMAL STOPPING RULES. 

references: Thomas S. Ferguson, Optimal Stopping and Applications

14.03.2012, Paweł Wanat 
Optimal Stopping and Applications 2 

Chapter 4. Applications. Markov Models. 

references: Thomas S. Ferguson, Optimal Stopping and Applications

07.03.2012, Jonasz Pamuła 
Optimal Stopping and Applications 1 

First chapters of the book Optimal Stopping and Applications, by Thomas S. Ferguson. 
29.02.2012, Jakub Kozik 
Property B  two coloring of uniform hypergraphs. 

m(n) is defined to be the smallest number for which there exists an nuniform hypergraph with m(n) edges which is not 2colorable. Erdos and Lovasz conjectured that m(n) asymptotically behaves like n 2^n. I will present a simple proof of the best known lower bound sqrt(n/log(n)) 2^n, originally derived by Radhakrishnan and Srinivasan in 2000.

18.01.2012, Michał Marczyk 
Unification through Projectivity by S. Ghilardi 

We introduce an algebraic approach to Eunification, through the notions of finitely presented and projective object. As applications and examples, we determine the unification type of varieties generated by a single finite quasiprimal algebra, of distributive lattices and of some other equational classes of algebras corresponding to fragments of intuitionistic logic. 
11.01.2012, Michał Marczyk 
Unification through Projectivity by S. Ghilardi 

We introduce an algebraic approach to Eunification, through the notions of finitely presented and projective object. As applications and examples, we determine the unification type of varieties generated by a single finite quasiprimal algebra, of distributive lattices and of some other equational classes of algebras corresponding to
fragments of intuitionistic logic. 
04.01.2012, Patryk Zaryjewski 
State complexity of power by Michael Domaratzki, Alexander Okhotin 

The number of states in a deterministic finite automaton (DFA) recognizing the language L^k where L is regular language recognized by an nstate DFA, and k>=2 is a constant, is shown to be at most n2^((k1)n) and at least (nk)2^((k1)(nk)) in the worst case, for every n > k and for every alphabet of at least six letters. Thus, the state complexity of L^k is Θ(n2^((k1)n)). In the case k=3 the corresponding state complexity function for L^3 is determined as (6n3)/8 4^n  (n1)2^n  n with the lower bound witnessed by automata over a fourletter alphabet. The nondeterministic state complexity of L^k is demonstrated to be nk. This bound is shown to be tight over a two letter alphabet.

21.12.2011, Dominik Dudzik 
Higher Order Matching and Games by Colin Stirling 

Assume simply typed lambda calculus with base type 0 and the definitions of αequivalence, β and ηreduction. A matching problem has the form v = u where v,u : A for some type A, and u is closed. The order of the problem is the maximum of the orders of the free variables x1,...,xn in v. A solution of a matching problem is a sequence of terms t1 ,..., tn such that v {t1/x1 ,..., tn/xn} =βη u.
We provide a gametheoretic characterisation of higherorder matching. The idea is suggested by model checking games. We then show that some known decidable instances of matching can be uniformly proved decidable via the gametheoretic characterisation.

14.12.2011, Adam Zydroń 
Spanning forests on the Sierpinski gasket 

We study the number of spanning forests on the Sierpinski gasket SGd(n) at stage n with dimension d equal to
two, three and four, and determine the asymptotic behaviors. The corresponding results on the generalized Sierpinski gasket SGd,b(n) with d = 2 and b = 3; 4 are obtained. We also derive upper bounds for the asymptotic growth constants for both SGd and SG2,b. 
07.12.2011, Michał Handzlik 
SOME IMPROVEMENTS TO TURNER'S ALGORITHM FOR BRACKET ABSTRACTION by M. Bunder 

A computer handles lambda terms more easily if these are translated into combinatory terms. This translation process is called bracket abstraction. The simplest abstraction algorithmthe (fab) algorithm of Curry (see Curry and Feys [6])is lengthy to implement and produces combinatory terms that increase rapidly in length as the number of variables to be abstracted increases.
A measure of the efficiency of an abstraction algorithm was first introduced by Kennaway as an upper bound of the length of the obtained combinatory term, as a function of the length of the original term and the number of variables to be abstracted. Mulder used these methods and experiments with many special cases, to compare the efficiency of the main algorithms listed above. The algorithm of Statman came out as the most efficient in the limiting case, but showed up as almost the worst in a number of reasonably simple special cases. Turner's algorithm was generally the best in these cases and was in fact Mulder's choice overall. In this paper, firstly we note that what Turner describes as "the improved
algorithm of Curry", on which his own is based, is in fact not equivalent to any of Curry's algorithms. Turner's abstracts lack a basic property possessed by all of
Curry's as well as many others. Secondly we give methods whereby Turner's algorithm (as well as others) can be
more efficiently implemented, while providing simpler abstracts. 
30.11.2011, Piotr Wójcik 
A note on propositional proof complexity of some Ramseytype statements by Jan Krajicek 

A Ramsey statement denoted n > (k, 2, 2) says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into valid DNF formula RAM(n, k) of size O(n^k) and with terms of size {k \choose 2}. Let r_k be the minimal n for which statement holds. We prove that RAM(r_k, k) requires expotential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll.

23.11.2011, Jakub Kozik 
Optimal stopping for covert expansion. 


16.11.2011, Michał Masłowski 
Coarsegraining of cellular automata, emergence, and the predictability by Navot Israeli, Nigel Goldenfeld 

Using nearest neighbor, onedimensional Cellular Automata (CA), we show how to construct local coarsegrained escriptions of CA with different complexity classification. Largescale behavior can be emulated by them without smallscale details. We show that coarsegrained CA can be decidable even for universal original systems and coarsegraining transformations make a complexity hierarchy of CA rules. Finally we argue that the large scale dynamics of CA can have very small Kolmogorov complexity of the update rules, and moreover exhibits a novel scaling law. This makes finding coarsegrained descriptions of CA easier at coarser scales. We interpret this large scale simplicity as a pattern formation mechanism in which large scale patterns are forced upon the system by the simplicity of the rules that govern the large scale dynamics. 
09.11.2011, Marek Wróbel 
Complexity of Type Inference by Jerzy Tyszkiewicz 

The type inference problem may be stated as follows: given a term of untyped lambda calculus, decide whether it may be typed to a term of a firstordertyped lambda calculus. If it is possible, then find all possible typings for it (or at least one possible typing). We show that the type inference problem is PTIMEcomplete. 
02.11.2011, Przemysław Jedynak 
How common can be universality in cellular automata? by Guillaume Theyssier 

We address the problem of the density of intrinsically universal cellular automata among cellular automata or a subclass of cellular automata. We show that captive cellular automata are almost all intrinsically universal. We show however that intrinsic universality is undecidable for captive cellular automata. Finally, we show that almost all cellular automata have no nontrivial subautomaton. 
26.10.2011, Maciej Bendkowski 
On Post correspondence problem for letter monotonic languages by Vesa Halava, Jarkko Kari, Yuri Matiyasevich 

We prove that for given morphisms g, h: { a_1, ..., a_n } \to B^{*}, it is decidable whether or not there exists a word w in the regular language a_{1}^{*}, ..., a_{n}^{*} such that g(w) = h(w). In other words, we prove that the Post Correspondence Problem is decidable if the solutions are restricted to be from this special language. This yields a nice example of an undecidable problem in integral matrices which cannot be directly proved undecidable using the traditional reduction from the Post Correspondence Problem. 
19.10.2011, 12.10.2011, Robery Obryk 
Dowodzenie w językach z typami zależnymi 

Celem systemów typów w językach programowania jest ułatwianie wnioskowania o poprawności kodu. Już języki używające systemu typów HindleyaMilnera pozwalają wnioskować w ciekawy sposób o zachowaniu funkcji na
podstawie ich typu. Języki z typami zależnymi pozwalają wyrażać za pomocą typu funkcji praktycznie arbitralne warunki na jej zachowanie. Na tym seminarium poznamy
formalizm typów zależnych, sposób przeprowadzania izomorfizmu CurryegoHowarda w nim i przyjrzymy się jak typy zależne pozwalają dowodzić własności programu
i pomagają w dowodzeniu własności stopu w języku Agda. 
05.10.2011, Robert Obryk 
Dowodzenie w językach z typami zależnymi 

Celem systemów typów w językach programowania jest ułatwianie wnioskowania o poprawności kodu. Już języki używające systemu typów HindleyaMilnera pozwalają wnioskować w ciekawy sposób o zachowaniu funkcji na
podstawie ich typu. Języki z typami zależnymi pozwalają wyrażać za pomocą typu funkcji praktycznie arbitralne warunki na jej zachowanie. Na tym seminarium poznamy
formalizm typów zależnych, sposób przeprowadzania izomorfizmu CurryegoHowarda w nim i przyjrzymy się jak typy zależne pozwalają dowodzić własności programu
i pomagają w dowodzeniu własności stopu w języku Agda.
Tematy do nastęnych seminariów:
"A Predicative Analysis of Structural Recursion" Abel, Altenkirch
"The SizeChange Principle for Program Termination" Lee, Jones, BenAmran 
01.06.2011, Małgorzata Kruszelnicka 
Bisymulation on finite Kripke models 

The notion of bisimulation has been introduced to test whether two processes behave the same. Originally discovered in Computer Science, bisimulation nowadays is employed in many fields. Today it is used in a number of areas of Computer Science such as functional languages, data types, databases, program analysis, to name but a few. Growing interests in this notion led to the discovery of bisimulation in Modal Logic and Set Theory. Finally, the notion was introduced into firstorder logic, and found a straightforward gametheoretical interpretation.
We present the notion of bisimulation for intuitionistic logic. Our discussion focuses on two cases: the propositional and the firstorder case. In both cases we present the theorem which states that bisimulation implies logical equivalence, and consider possible variants of the inverse implication. Further, we present our contribution to the research of the inverse theorem.
References:
Patterson, A.: \emph{Bisimulation and Propositional Intuitionistic Logic}, Proceedings of the 8th International Conference on Concurrency Theory, SpringerVerlag, 1997
Po{\l}acik, T.: \emph{Back and Forth Between FirstOrder Kripke Models}, Logic Journal of the IGPL 16 (4), 335355, 2008
Visser, A.: \emph{Bisimulations, Model Descriptions and Propositional Quantifiers}, Logic Group Preprint Series 161, 1996

25.05.2011, Agnieszka Łupińska 
A Universal Approach to SelfReferential Paradoxes, Incompleteness and Fixed Points, by Noson S. Yanofsky 

kontynuacja 

references:

18.05.2011, Agnieszka Łupińska 
A Universal Approach to SelfReferential Paradoxes, Incompleteness and Fixed Points, by Noson S. Yanofsky 

Following F. William Lawvere, we show that many selfreferential paradoxes, incompleteness theorems and fixed point theorems fall out of the same simple scheme. We demonstrate these similarities by showing how this simple scheme encompasses the semantic paradoxes, and how they arise as diagonal arguments and fixed point theorems in logic, computability theory, complexity theory and formal language theory. 
11.05.2011, Robert Obryk 
Algorithmic Information Theory 2, by Gregory. J. Chaitin 



references:

04.05.2011, Robert Obryk 
Algorithmic Information Theory , by Gregory. J. Chaitin 


27.04.2011, 20.04.2011, Marek Wróbel, Adam Zydroń 
Mathematics for the Analysis of Algorithms  Asymptotic Analysis 


13.04.2011, 06.04.2011, Maciej Bendkowski 
Mathematics for the Analysis of Algorithms  Operator Methods 


30.03.2011, Michał Masłowski, Tomasz Bińczycki 
kontynuacja 


23.03.2011, Anna Bień (UŚ) 
Klasy grafów singularnych 

We consider simple graphs and their adjacency matrices. In [1] Rara gives graphs with singular adjacency matrix are called singular. In [1] Rara presented tools, which are useful in computing determinant of adjacency matrix of some simple graphs. Rara's methods allow to replace complicated algebraic calculations with operations performed on graphs. In some cases removing sets of edges or vertices does not change or changes the determinant of a graph in a specific way. We continue this subject matter and present general methods of reducing graphs. The most general is the method of identifying $P_3$ paths.
Consequences of this theorem are the method of contracting $P_5$ path and a method which can be applied to graphs circumscribed on cycles. We apply these methods in computing determinant of adjacency matrix of certain classes of graphs. In particular we present a recursive formula for planar grids $P_n \times P_{n+1}$
$$det A(P_n \times P_{n+1})= (1)^{(n+1)/2}$$
which is a main step in solution of the singularity problem for all planar grids.
[1] H.M. Rara, Reduction procedures for calculating the determinant of the adjacency matrix of some graphs and
the singularity of square planar grids, Discrete Mathematics 151, 213219, Elsevier, 1996. 
16.03.2011, 09.03.2011, Michał Masłowski 
Mathematics for the Analysis of Algorithms  Recurrence Relations 


02.03.2011, Tomasz Bińczycki 
Mathematics for the Analysis of Algorithms  Binomial Identities 


19.01.2011, Przemek Jedynak 
Synthetic Differential Geometry  Chicago's pizza seminar notes. 


12.01.2011, Tomasz Krakowiak 
Complexity of Type Inference, paper by Jurek Tyszkiewicz 

The main result is the proof of PTIMEcompleteness of the type reconstruction problem for simply typed lambda calculus.

05.01.2011, Patryk Zaryjewski 
Interaction properties of relational periods, paper by Vesa Halava and Tero Harju and Tomi K¨arkiy 

We consider relational periods where the relation is a compatibility relation on words induced by a relation on letters. We introduce three types of periods, namely global, external and local relational periods, and we compare their properties by proving variants of the theorem of Fine and Wilf for these periods.

15.12.2010, Jacek Bąkowski 
On systems of word equations ..., paper by Elena Czeizler, and Wojciech Plandowski 

In this paper, we investigate the open question, formulated in 1983 by Culik II and Karhumäki, asking whether there exist independent systems of three word equations over three unknowns admitting nonperiodic solutions. In particular, we answer negatively the
above mentioned question for systems in which one of the unknowns occurs at most six times. That is, we show that such systems admit only periodic solutions or they are not
independent.

08.12.2010, Hannes Diener (Univ. of Siegen, Germany) 
Variations on a theme by Ishihara 

This will be a talk in two halves. The first will consist of a gentle introduction to the area of constructive analysis, especially focussing on continuity and completeness. In constructive mathematics one is interested
in objects that one cannot only rule out the nonexistence of, but those that one can (at least in theory) actually construct. This part of the talk should be accessible to anyone with a knowledge of basic analysis  no knowledge about constructivism is required.
In the second half we will present results by Hajime Ishihara of 1991, which became known as ``Ishihara's tricks''. In these results decisions that, on first and maybe even second glance, seem algorithmically impossible are made. We will present new results, which extend Ishihara's ideas to a more general setting. Lastly, we will show how all of this can be used to give an axiomatic, concise, and clear proof of the well known phenomenon that in many constructive settings every realvalued function on the unit interval is continuos (``computability implies continuity''). 
01.12.2010, Paweł Błasiak (IFJ Kraków) 
Combinatorial Models of CreationAnnihilation 

Quantum physics has revealed many interesting formal properties associated with the algebra of two operators, A and B, satisfying the partial commutation relation
ABBA=1. We surveys the relationships between classical combinatorial structures and the reduction to normal form of operator polynomials in such an algebra. The connection is achieved through suitable graphs, or ''diagrams'', that are composed of elementary ''gates''. In this way, many normal form evaluations can be systematically obtained, thanks to models that involve set partitions, permutations, increasing trees,
etc.
Reference:
P. Blasiak and Ph. Flajolet
"Combinatorial Models of CreationAnnihilation"
arXiv:1010.0354 [math.CO]

24.11.2010, Michał Handzlik 
Pseudotopological spaces and the StoneCech compactification. 

Our slogan is "topology is about convergence". The fact that so many aspects of topology can be captured by convergence naturally makes us wonder whether convergence could be taken to be more fundamental than open sets. It leads to the definition od pseudotopological space, where we focus on convergence properties only, without mentioning open sets. We present how StoneCech compactification translates into pseudotopological spaces.

17.11.2010, Jonasz Pamuła 
Algorithms for learning regular expressions from positive data, paper by Henning Fernau 

We describe algorithms that directly infer very simple forms of 1unambiguous regular expressions from positive data. Thus, we characterize the regular language classes that can be learned this way, both in terms of regular expressions and in terms of (not necessarily minimal) deterministic finite automata. 
10.11.2010, Ola Piktus 
Topology on words, paper by Cristian S. Calude, Helmut Jürgensen, Ludwig Staiger 

We investigate properties of topologies on sets of finite and infinite words over a finite alphabet. The guiding example is the topology generated by the prefix relation on the set of finite words, considered as a partial order. This partial order extends naturally to the set of infinite words; hence it generates a topology on the union of the sets of finite and infinite words. We consider several partial orders which have similar properties and
identify general principles according to which the transition from finite to infinite words is natural. We provide a uniform topological framework for the set of finite and infinite words to handle limits in a general fashion. 
03.11.2010, 27.10.2010, Kasia Grygiel 
Asymptotically almost all lambda terms are strongly normalizing 

We present quantitative analysis of various (syntactic and behavioral) properties of random lambda terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the lambda calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This
is due to the fact that any fixed combinator almost always appears in a random combinator. 
20.10.2010, Piotr Faliszewski (AGH) 
A 2Approximation Algorithm for a Candidate Promotion Problem 

We are given an election E=(C,V), where C is a set of alternatives, and V is a collection
of voters, and a preferred alternative p. Each voter is represented by a linear order over C.
As part of a political campaign, we have the ability (at some cost) to shift p forward in some of the votes. In the shiftbribery problem we ask for the minimal cost of shifts that ensure our candidate's victory. We show that this problem is NPcomplete (for Borda winner determination
rule; an example of socalled scoring rules) and give a 2approximation algortihm that works for all scoring rules, even if the votes are weighted.

13.10.2010, Kuba Kozik 
Recent progress in bestchoice problems for posets. 


02.06.2010, Jan Hązła 
Denotational semantics of T 


26.05.2010, Maria Chmaj 
Coherent Spaces 


21.04.2010, Karol Kosiński 
Sequent calculus, chapter 5 of Girard's book. 


14.04.2010, Rafał Pajdzik 
The Normalization Theorem, Chapter 4 of Girard's book. 


07.04.2010, Leszek Horwath (Cedric) 
Curry Howard Isomorphism. Chapter 3 of Girard's book. 


24.03.2010, 10.03.2010, Szymon Borak 
Fixed point theory for programs 


28.01.2010, ZAJĘCIA W NOWYM SEMESTRZE 
PROOFS AND TYPES 

Link do książki Girarda pt. Proofs and Types.
List of chapter titles:
1. Sense, Denotation and Semantics
2. Natural Deduction
3. The CurryHoward Isomorphism
4. The Normalisation Theorem
5. Sequent Calculus
6. Strong Normalisation Theorem
7. Gödel's system T
8. Coherence Spaces
9. Denotational Semantics of T
10. Sums in Natural Deduction
11. System F
12. Coherence Semantics of the Sum
13. Cut Elimination (Hauptsatz)
14. Strong Normalisation for F
15. Representation Theorem
Appendices:
A. Semantics of System F  by Paul Taylor
B. What is Linear Logic?  by Yves Lafont

27.01.2010, Marek Wróbel 
Program Analysis 

Ostatnia część książki Changa and Lee o dowodzeniu twierdzeń. 
20.01.2010, Michał Handzlik 
Procedury dowodowe oparte na twierdzeniu Herbranda 

Rozdział 9. książki Changa i Lee o automatycznym dowodzeniu twierdzeń. 
06.01.2010, Maria Chmaj 
Równość 

Rozdział 8. książki Changa i Lee o automatycznym dowodzeniu twierdzeń. 
16.12.2009, Jan Hązła 
Linear Resolution in FOL 

Rozdział 7. książki Changa & Lee. 
02.12.2009, Adam Zydro 
Semantic Resolution 

Rozdział 6. ksiązki Changa & Lee. 
25.11.2009, Piotr Faliszewski 
Distance Rationalizability of Voting Rules 

A voting rule is an algorithm for determining the winner in an election.
One can easily come up with many different voting rules, but it is also important to justify why a given rule is natural/useful. There are several approaches that have been used to justify the proposed rules. One justification is to show that a rule satisfies a set of desirable axioms that uniquely identify it. Another is to show that the calculation that it performs is actually maximum likelihood estimation relative to a certain model of noise that affects voters (MLE approach). The third approach, which has been recently actively investigated, is the socalled distance rationalizability framework. In it, a voting rule is defined via a class of consensus elections (i.e., a class of elections that have a clear winner) and a distance function. A candidate c is a winner of an election E if c wins in one of the consensus elections that are closest to E relative to the given distance. In this talk, we show that essentially any voting rule is distancerationalizable if we do not restrict the two ingredients of the rule: the consensus class and the distance. Thus distance rationalizability of a rule does not by itself guarantee that the voting rule has any desirable properties. However, we demonstrate that the distance used to rationalize a given rule may provide useful information about this rule's behavior. Specifically, we identify a large class of distances, which we call votewise distances, and show that if a rule is rationalized via a distance from this class, many important properties of this rule can be easily expressed in terms of the underlying distance. This enables us to provide a new characterization of scoring rules and to establish a connection with the MLE framework. We also give bounds on the computational complexity of the winner determination problem for distancerationalizable rules.

18.11.2009, Sylwia Antoniuk 
Rezolucja 

Rezolucja jako rewolucja, w relacji do rewelacji. 
04.11.2009, Rafał Pajdzik, UJ 
FOL 

Chapters 3,4 on First Order Logic from `Symbolic Logic and Mechanical Theorem Proving' by ChinLiang Chang and Richard CharThung Lee. 
28.10.2009, Marek Zaionc 
Schwichtenberg style lambda definability is undecidable 


21.10.2009, Mareusz Drewienkowski, UJ 
Gry w wielomiany (Playing polynomials) 

We will hear about the process of reconstruction of polynomials from the finite number of examples. The talk is based on the 1997 paper by J. Małolepszy, M. Moczurad and M. Zaionc entitled "Schwichtenberg style lambda definability is undecidable" published in Lecture Notes in Computer Science 1210, pp. 267283. 
14.10.2009, Marek Zaionc 
Two open problems on lambda definability 

We discus two open lambda definability problems.
1. It can be shown that any lambda definable operation on numbers can be synthesize from the finite number of examples. We will discuss the same problem for lambda definable word operations.
2. We address the problem of lambda definable tree operations. Is it true that the set of all lambda definable tree operations is NOT finitely generated.

03.06.2009, Jakub Kozik 
Drzewa and/or  przegląd problemów 


27.05.2009, Paweł Waszkiewicz 
T^omega as a universal domain 

Following G. Plotkin [T^omega as a universal domain, J. of Comp. and System Sci. 17, 1978] We introduce a domain T^omega and a language LAMBDA, and show that LAMBDAdefinability coincide with computability. Furthermore, we show that T^omega is universal, in the sense that every boundedcomplete dcpo embeds in it. Finally, we demonstrate that every secondcountable T_0 space topologically embeds in T^omega as an isochordal subspace.

13.05.2009, Wojciech Czarnecki 
The CurryHoward Isomorphism 


06.05.2009, 29.04.2009, Michał Klasiński 
Wśród typów nie ma arystokracji 


22.04.2009, 15.04.2009, Sylwia Antoniuk 
Basic Simple Type Theory 


08.04.2009, 01.04.2009, Michał Handzlik 
Higherorder Unificatrion and Matching 


25.03.2009, 11.03.2009, Paweł Waszkiewicz 
A Lazy Introduction to Goedel's Theorems 

See http://www.logicmatters.net/
for more info. 
21.01.2009, Mateusz Kostanek 
Regular Languages and Stone Duality 

We give a new account of the relationships among varieties of regular languages, varieties of finite semigroups, and their characterization in terms of "implicit identities." Our development, which is essentially topological in character, is based on the duality (established by Stone) between Boolean algebras and certain topological spaces (which are now called "Stone spaces"). This duality does not
seem to have been recognized in the literature on regular languages, even though it is well known that the regular languages over a fixed alphabet form a Boolean algebra and that the "implicit operations" with a fixed number of operands form a Stone space.
Na podstawie artykulu: N. Pippenger, Regular Languages and Stone Duality, Theory Comput. Systems30, 121134 (1997).

07.01.2009, Michał Pokrywka 
Algorytmy kolejkowania danych w sieciach komputerowych 

cd z poprzedniego roku. 
17.12.2008, Michał Pokrywka 
Algorytmy kolejkowania danych w sieciach komputerowych 

Przedstawię dwie publikacje godne uwagi opisujące modele matematyczne dwóch rozwiązań. Jedna dotyczy algorytmu RED (Random Early Detection) a druga HFSC (Hierarchical Fair Service Curve).
Algorytm RED pozwala w sieciach wysokich prędkości na zapobieganie zdominowaniu pasma przez jeden strumień danych za pomocą losowego odrzucania pakietów (z prawdopodobieństwem ważonym).
Algorytm HFSC pozwala dla kolejki danych zdefiniować parametry ,,krzywych usług'' (ang. service curves) do dynamicznego sprawiedliwego podziału pasma, zachowując parametry strumieni realtime.

29.10.2008, Mateusz Drewienkowski 
Dualność Stone'a  cz.2. 


22.10.2008, Mateusz Drewienkowski 
Dualność Stone'a  cz.1. 


15.10.2008, Jarosław Duda 
Asymmetric numeral systems 

We will speak about new approaches to entropy encoding. We present various generalizations of standard numeral systems which are optimal for encoding sequences of equiprobable symbols as asymmetric numeral systems  optimal for freely chosen probability distributions of symbols. It has some similarities to Range Coding but instead of encoding a symbol in choosing a range, we spread these ranges uniformly over whole interval. This leads to a simpler en
coder  instead of using two states to define range, we need only one. This approach is truly universal  we can get from extremely precise encoding (ABS) to extremely fast with possibility to additionally encrypt the data (ANS).
This encryption uses a key to initialize a random number generator, which is used to calculate the coding tables. Such preinitialized encryption has an additional advantage: it's resistant to brute force attack  in order to check a key we have to make the whole initialization. We will also show that using ANS we can get an error correction method which is resistant to pessimistic cases. 
04.06.2008, Mateusz Kostanek 
Quantale semantics of linear logic (2) 


28.05.2008, Kenetsu Fujita, Shimane Univ. Japan 
A translation from lambda2 into lambda_exists 

This talk shows that there exist translations between
polymorphic lambda calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic lambda calculus into the existential type system is the socalled callbyname CPStranslation that can be expounded as an adjoint from the neat connection. The construction of an inverse translation is investigated from a viewpoint of residuated mappings. The duality appears not only in the reduction relations but also in the proof structures such as paths between the source and the target calculi.
From a programming point of view, this result means that
abstract data types can interpret polymorphic functions
under the CPStranslation. We may regard abstract data types
as a dual notion of polymorphic functions. This talk is based on an extended and improved version of the paper
presented at TLCA2005.

21.05.2008, Mateusz Kostanek 
Quantale semantics for linear logic 


14.05.2008, Jakub Kozik 
Realizability 


07.05.2008, Bożena Woźna, Akademia im. Jana Długosza, Częstochowa 
Ograniczona Weryfikacja Modelowa dla systemów wieloagentowych i systemów z czasem 

W referacie przedstawię wyniki moich badań w zakresie automatycznej weryfikacji modelowej systemów czasu rzeczywistego oraz systemów wieloagentowych.
Wyniki te zostały osiągnięte we współpracy z prof. Wojciechem Penczkiem (IPI PAN Warszawa),
dr Andrzejem Zbrzeznym (AJD, Częstochowa) oraz dr Alessio Lomuscio (UCL, Londyn). W szczególności opowiem o zaproponowanej przeze mnie Ograniczonej
Weryfikacji Modelowej, którą zastosowałam zarówno do systemów z czasem jak i systemów wieloagentowych.
Zrobię również krótkie wprowadzenie do formalizmów stosowanych w automatycznej weryfikacji modelowej wy?ej wymienionych systemów.
System czasu rzeczywistego to (zgodnie z definicją IEEE) system, którego poprawność działania zależy nie tylko od poprawności logicznych rezultatów, lecz również od czasu, w jakim te rezultaty są osiągane.
Systemy czasu rzeczywistego znajdują zastosowanie między innymi w przemyśle do nadzorowania procesów technologicznych, przy implementacji
protokołów komunikacyjnych, w planowaniu i kontroli ruchu lotniczego, itd.
Agent to jednostka, która działa w pewnym ustalonym środowisku, jest zdolna do komunikowania się, monitorowania swego otoczenia i podejmowania autonomicznych decyzji.
System wieloagentowy to sieć komunikujących się i współpracujących między
sobą agentów,
realizujących zarówno wspólne jak i prywatne cele.
Systemy wieloagentowe mają już swoją ugruntowaną pozycję
w wielu dziedzinach związanych z technologią informacji, np.: w inżynierii oprogramowania, ehandlu, sieciach telekomunikacyjnych,
automatycznym wnioskowaniu i argumentacji, wspomaganiu zarządzaniem w
przedsiębiorstwie, itd.
Weryfikacja modelowa jest jedną z najbardziej rozpowszechnionych
metod automatycznej weryfikacji poprawności systemów czasu rzeczywistego
oraz systemów wieloagentowych. Pierwsze prace na ten temat
ukazały się w 1981 roku i od tamtego czasu trwa nieustanny rozwój narzędzi wykorzystujących udoskonalane algorytmy.
Różnorodność dostępnych podejść, jak też rozwiązań,
jest wynikiem istnienia wielu modeli dla wyżej wymienionych systemów, np.
przeplotowych i nieprzeplotowych, jak też wielu metod opisu własności tych
systemów, np. poprzez automaty, algebry procesów lub logiki temporalne.
Istotny postp w dziedzinie weryfikacji dokonał się w 1990 roku po
opracowaniu metod bazujących
na obliczeniach symbolicznych, wykorzystujących formalizm Boolowskich
Diagramów Decyzyjnych.
Następny krok do przodu został wykonany w 1999 roku po sprowadzeniu problemu
weryfikacji modelowej do problemu testowania spełnialności dla formuł
zdaniowych i wykorzystaniu efektywnych algorytmów dla tego ostatniego
problemu.

23.04.2008, Mateusz Juda 
Arytmetyka Heytinga 

Na podstawie skryptu Thomasa Streichera (patrz poprzednie referaty tego samego autora). 
16.04.2008, Tomasz Połacik, Uniw. Śląski 
Modele Kripkego dla teorii pierwszego rzędu 

Druga część referatu jest poświęcona modelom Kripkego dla logiki pierwszego rzędu. Omówimy podstawowe własności modeli i twierdzenie o pełności. Przedstawimy w niej również rezultaty dotyczące konstrukcji modeli Kripkego dla intuicjonistycznych teorii pierwszego rzędu, ze szczególnym uwzglednieniem Arytmetki Heytinga.

09.04.2008, Tomasz Połacik, Uniw. Śląski 
Modele Kripkego dla intuicjonistycznej logiki zdań 

W pierwszej części referatu zajmiemy się zagadnieniami związanymi z modelami Kripkego dla intuicjonistycznej logiki zdań. Poza podstawowymi własnościami i intuicjami dotyczącymi modeli, przedstawione zostanie twierdzenie o pełności Rachunku Heytinga względem semantyki kripkowskiej. Omówimy też najważniejsze konstrukcje modeli Kripkego i pokażemy semantyczne dowody niektórych własności Rachunku Heytinga.

02.04.2008, Paweł Waszkiewicz 
O analizie infinitezymalnej w światach gładkich 

Zanim zaproponowano pojęcie granicy, matematycy tacy jak Fermat czy Leibnitz posługiwali się w dowodach swoich twierdzeń analitycznych pojęciem wartości nieskończenie małych. Podczas seminarium opowiem o rachunku wartości nieskończenie małych, który przypomina metody analityczne sprzed 350400 lat, ale  w odróżnieniu od nich  jest doskonale precyzyjny. Modele tego rachunku nz. światami gładkimi. Co czyni światy gładkie ciekawymi jest m.in. fakt, iż w takim świecie prosta rzeczywista R jest prawdziwym continuum, tzn. nie można z niej wydzielić żadnego nietrywialnego podzbioru. (Podzbiór U wydziela się z R, jeśli dla każdego x z R albo x należy do U, albo x nie należy do U.)
Wykład przygotowałem na podstawie: J.L.Bell, A Primer on Infinitesimal Analysis, Cambridge Univ. Press, 1998. Google: ,,John L. Bell''. Warto.

19.03.2008, Mateusz Juda 
Introduction to Constructive Logic and Mathematics (II) 

Omawiamy kolejne tematy ze skryptu Thomasa Streichera. Dzisiaj:
 Constructive Arithmetic and Analysis
 Constructive Real Numbers 
12.03.2008, Jakub Kozik 
Jak wiele formuł ma konstruktywne dowody? 

W referacie przedstawię wyniki otrzymane z A. Genitrini dotyczące ilościowego porównania zdaniowych logik: klasycznej i intuicjonistycznej. W rozważanych formułach dopuszczamy wszystkie zwykle używane łączniki (koniunkcja, alternatywa, implikacja) oraz stałą "absurd" (bottom). Nasz główny wynik można nieformalnie wypowiedzieć jako: "około 5/8 tautologii logiki klasycznej ma konstruktywne dowody." Ciekawym wynikiem dodatkowym jest zgodność dwóch, pozornie niezależnych, metod liczenia gęstości.

05.03.2008, Mateusz Juda 
Introduction to Constructive Logic and Mathematics (I) 

Mateusz referuje pierwszą część skryptu Thomasa Streichera, pod tym samym tytułem, dostępnego TUTAJ.
Możemy spodziewać się następujących zagadnień:
 Natural Deduction for Constructive Logic
 A Hilbert Style System for CL
 Truth–Value Semantics of CL
 Embedding Classical into CL
(Constructive = Intuitionistic)

27.02.2008, Paweł Waszkiewicz 
Konstruktywizm wg Bridgesa. Piękno wg Patarai. 

Tematem naszego seminarium w tym semestrze jest konstruktywizm i intuicjonizm. Podczas pierwszego spotkania przedstawię artykuł Douglasa Bridgesa pt. Reality and Virtual Reality in Mathematics, w którym autor daje nam krótki kurs historii matematyki konstruktywnej. Aby zniszczyć humanistyczny nastrój, który nieuchronnie wytworzy się podczas wykładu historycznego, zakończę twardym, ale konstruktywnym dowodem faktu, że każda funkcja monotoniczna f:X>X na posecie zupełnym X, wyposażonym w element najmniejszy, posiada najmniejszy punkt stały. Dowód, pochodzący od gruzińskiego matematyka Dimitriego Patarai, nie używa liczb porządkowych. 
23.01.2008, Kacper Marcisz 
An application of stream calculus to signal flow graphs 

Pan Kacper referujr artykuł Jana Ruttena pod tym samym tytułem. Dane bibliograficzne artykułu: Proceedings FMCO 2003 (Formal Methods for Components and Objects). Editors: F.S. de Boer, M.M. Bonsangue, S. Graf, W.P de Roever. Lecture Notes in Computer Science 3188, Springer Verlag, 2004, pp. 276291.
Jest to kontynuacja tematyki przedstawionej przez panią Dominikę Majsterek wcześniej na naszym seminarium.

16.01.2008, Szymon Wójcik 
Parallel reductions in lambda calculus 

The notion of parallel reduction is extracted from the simple proof of the ChurchRosser theorem by Tait and MartinLöf. Intuitively, this means to reduce a number of redexes (existing in a lambda term) simultaneously. During the talk, after reevaluating the significance of the notion of parallel reduction in TaitandMartinLöf type proofs of the ChurchRosser theorems, we show that the notion of parallel reduction is also useful in giving short and direct proofs of some other fundamental theorems in reduction theory of lambda
calculus. 
09.01.2008, Dominika Majsterek UJ 
Behavioural differential equations: a coinductive calculus (część 2) 

Pani Dominika referuje artykuł: J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science vol. 308(13), pp. 153, 2003. 
19.12.2007, Mikołaj Bojańczyk, Instytut Informatyki, Uniwersytet Warszawski 
Automaty ścieżkowe 

Automat ścieżkowy to rodzaj automatu skończonego na drzewach. W odróżnieniu od powszechnie używanych automatów na drzewach, automat taki przetwarza drzewo sekwencyjnie, a nie równolegle. Pokażę, że automat ścieżkowy mało potrafi.

12.12.2007, Dominika Majsterek 
Behavioural differential equations: a coinductive calculus 

Pani Dominika referuje artykuł: J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science vol. 308(13), pp. 153, 2003.
Abstract: We present a theory of streams (infinite sequences), automata and languages, and formal power series, in terms of the notions of homomorphism and bisimulation, which are cornerstones of the theory of (universal) coalgebra. This coalgebraic perspective leads to a unified theory, in which the observation that each of the aforementioned sets carries a socalled final automaton structure, plays a central role. Finality forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. Coinductiove definitions take the shape of what we have called behavioural differential equations, after Brzozowski's notion of input derivative. A calculus is developed for coinductive reasoning about all of the aforementioned stuctures, closely resembling calculus from classical analysis.

05.12.2007, Tytus Bierwiaczonek 
Logical aspects of finite automata 

Pan Tytus referuje przeglądowy artykuł Wolfganga Thomasa pt. Languages, Automata and Logic. Usłyszymy o zależnościach pomiędzy automatami i monadyczną logiką drugiego rzędu.
Artykul dostępny jako [Tho96] na stronie
http://www.automata.rwthaachen.de/publications/pubThomas.html
albo od razu
tutaj . 
28.11.2007, Thierry Joly 
Undeciding lambdadefinability again 

The Definability Problem (DP for short) is the question whether a given functional of some hereditarily finite type structure over a single atomic type is the interpretation of a closed lambdaterm or not. DP was first considered about Full Type Structures by G. Plotkin in 1973, [Plo73]. R.Statman [Sta82] pointed out that deciding it would solve at once quite a few existential problems of the typed lambdacalculus, the most famous of which is the (still open) Matching Problem: "Given lambdaterms A, B, is there a lambdaterm X such that AX=B?" Then DP became a little Graal, finally proved undecidable by R. Loader in 1993, [Loa01]. Is that the end of the story? One may object that in smaller models than the Full Type Structures, the few lambdadefinable functionals would not be so easily
lost and that deciding definability in any class of (smaller) models that is strongly complete with respect to the lambdacalculus (in the sense of [Sta82]) would also yield the benefits pointed out by Statman. Unfortunately, we will show in this talk that the restriction of DP to a fixed model M is actually undecidable for a fair amount of models M, including all the non trivial stable models and order extensional models, except possibly the 2 element Scott model. These stronger results were obtained by cleaning previous proofs and by identifying their efficient ingredients. This work of simplification also yields a particularly short and easy proof of the undecidability of DP for Church pure typed lambdacalculus that will first be detailed.
[Plo73] Gordon Plotkin. Lambdadefinability and logical relations. Memorandum SAIRM4, University of Edinburgh, 1973.
[Sta82] Richard Statman. Completeness, invariance and lambdadefinability. JSL 47:1726, 1982.
[Loa01] Ralph Loader. The Undecidability of lambdaDefinability. In Logic, Meaning and Computation: Essays in Memory of A. Church, 331342, Anderson & Zeleny editors, Kluwer Acad. Publishers, 2001. 
21.11.2007, Tomasz Połacik, Instytut Matematyki, Uniwersytet Śląski, Katowice 
Problemy modeli Kripkego dla teorii pierwszego rzędu 

Jest faktem ogólnie znanym, że modele Kripkego stanowią ważne i efektywne narzędzie służące do badania intuicjonistycznych teorii pierwszego rzędu. Na przykład, znane są ich liczne interesujące zastosowania w przypadku takich konstruktywnych teorii jak arytmetyka Heytinga czy intuicjonistycza teorii mnogości KripkegoPlatka. Na uwagę zasługuje jednak fakt, że w przeciwieństwie do sytuacji teorii modeli klasycznych, wciąż brakuje ogólnych metod i konstrukcji dla modeli Kripkego.
Przypomnijmy, że  nieformalnie  na model Kripkego możemy patrzeć jak na rodzinę klasycznych modeli dla danego języka pierwszego rzędu, w której określony jest porządek wyznaczony przez homomorfizmy modeli tej rodziny. Na całej tej strukturze zdefiniowane jest pojęcie spełnialności. Przy czym, w odróżnieniu od klasycznej spełnialności (w sensie Tarskiego) traktowanej lokalnie, w pojedynczym modelu rozważanej rodziny, spełnialność zdefiniowana na modelu Kripkego jest spełnialnością intuicjonistyczną. Nietrudno jest zauważyć, że model Kripkego wyznaczony przez pojedynczy klasyczny model M z identycznościowym homomorfizmem może być utożsamiony z M widzianym jako model klasyczny. W tym sensie, pojęcie modelu Kripkego można uważać za uogólnienie klasycznego pojęcia modelu pierwszego rzędu. W sposób naturalny powstaje więc kwestia stosownego uogólnienia pojęć i związków klasycznej teorii modeli na przypadek modeli Kripkego.
Jedno z podstawowych zagadnień teorii modeli dotyczy elementarnej równoważności. W referacie rozważony zostanie problem elementarnej równoważności w odniesieniu do modeli Kripkego, a w celu jego rozwiązania, wprowadzone zostanie pojęcie bisymulacji dla modeli Kripkego pierwszego rzędu. Pojęcie to jest, z jednej strony, rozszerzenieniem pojęcia bisymulacji dla modeli Kripkego dla intuicjonistycznej logiki zdań oraz, z drugiej strony, uogólnieniem  w opisanym wyżej sensie  pojęcia gry Ehrenfeuchta dla klasycznych modeli pierwszego rzędu. Oprócz omówienia podstawowych własności bisymulacji, zostaną zaprezentowane również jej zastosowania. W szczególności, przedstawiona zostanie konstrukcja elementarnego podmodelu modelu Kripkego.

14.11.2007, Mateusz Kostanek 
Tree walking automata cannot be determinized 

Mateusz zreferuje artykul Mikołaja Bojańczyka i Thomasa Colcombeta, który otrzymał tytuł ,,best paper'' na konferencji ICALP 2004.
Abstrakt: Treewalking automata are a natural sequential model for recongnizing languages of finite trees. Such automata walk around the tree and may decide in the end to accept it. It is shown that deterministic treewalking automata are weaker than nondeterministic treewalking automata. 
07.11.2007, 24.10.2007, Mariusz Łusiak 
On learning monotone Boolean functions under the uniform distribution 

We prove two general theorems on monotone Boolean functions which are useful for constructing a learning algorithm for monotone Boolean functions under the uniform distribution. The first result is that a single variable function f(x) = x_i has the minimum correlation with majority function among all fair monotone functions. The second result is on the relationship between the influences and the average sensitivity of a monotone Boolean function.
The talk is based on a paper by Kazuyuki Amano and Akira Maruoka. 
17.10.2007, Mateusz Juda 
Automata for XML  A survey 

Mateusz referuje artykul Thomasa Schwenticka pod tym samym tytułem z Journal of Computer and System Sciences 73(2007), str. 289315. Abstract artykułu:
Automata play an important role for the theoretical foundations of XML data management, but also in tools for various XML processing tasks. This survey article aims to give an overview of fundamental properties of the different kinds of automata used in this area and to relate them to the four key aspects of XML processing: schemas, navigation, querying and transformation. 
03.10.2007, Jakub Kozik 
Intuitionistic versus Classical Tautologies 

We consider propositional formulas built on implication. The size of a formula is measured by the number of occurrences of variables. We assume that two formulas which differ only in the naming of variables are identical. For every n we investigate the proportion between the number of intuitionistic tautologies of size n compared with the number of classical tautologies of that size. We prove that the limit of that fraction is 1 when n tends to infinity. 