On June 20-21, 2005 the third workshop on *Computational Logic and Applications* took place in Chambéry after the ones in Lyon (June 2004) and in Krakow (June 2002). This workshop, funded by the French Rhone-Alpes region, brings together in a friendly atmosphere researchers from Poland and France around two main topics: analysis of algorithms and lambda calculus with type theory. These two topics, that at first look may seem disjoint, have a meeting point in research on the analysis of densities of lambda terms.

The proceedings of the former workshops have been published in Schedae Informaticae (for the Krakow meeting) and by ENTCS (for the Lyon meeting).

After their presentation at the workshop in Chambéry, some papers were submitted to the editors. The refereeing process (by two anonymous referees from all over the world) has been the usual one. This volume also includes the notes of the course given by Danièle Gardy on random boolean expressions.

We are happy to present these updated papers as a proceedings volume of DMTCS.

In sequential games of traditional game theory, backward induction guarantees existence of Nash equilibrium by yielding a sub-game perfect equilibrium. But if payoffs range over a partially ordered set instead of the reals, then the backward induction predicate does no longer imply the Nash equilibrium predicate. Non-determinism is a solution: a suitable non-deterministic backward induction function returns a non-deterministic strategy profile which is a non-deterministic Nash equilibrium. The main notions and results in this article are constructive, conceptually simple and formalised in the proof assistant Coq.

Section:
Proceedings

Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional programming languages. The original combinatory calculus corresponds to minimal implicative logic written in a system "à la Hilbert''. We present in this paper a combinatory logic which corresponds to propositional classical logic. This system is equivalent to the system $λ ^{Sym}_{Prop}$ of Barbanera and Berardi.

Section:
Proceedings

In this paper, we introduce the $λ μ ^{∧∨}$ - call-by-value calculus and we give a proof of the Church-Rosser property of this system. This proof is an adaptation of that of Andou (2003) which uses an extended parallel reduction method and complete development.

Section:
Proceedings

In this paper we prove that the question whether a language presented by a context free grammar has density, is undecidable. Moreover we show that there is no algorithm which, given two unambiguous context free grammars on input, decides whether the language defined by the first grammar has a relative density in the language defined by the second one. Our techniques can be extended to show that this problem is undecidable even for languages given by grammars from $LL(k)$ (for sufficiently large fixed $k ∈ \mathbb{N} )$.

Section:
Proceedings

An on-line vertex coloring algorithm receives vertices of a graph in some externally determined order. Each new vertex is presented together with a set of the edges connecting it to the previously presented vertices. As a vertex is presented, the algorithm assigns it a color which cannot be changed afterwards. The on-line coloring problem was addressed for many different classes of graphs defined in terms of forbidden structures. We analyze the class of $I_s$-free graphs, i.e., graphs in which the maximal size of an independent set is at most $s-1$. An old Szemerédi's result implies that for each on-line algorithm A there exists an on-line presentation of an $I_s$-free graph $G$ forcing A to use at least $\frac{s}{2}χ ^{(G)}$ colors. We prove that any greedy algorithm uses at most $\frac{s}{2}χ^{(G)}$ colors for any on-line presentation of any $I_s$-free graph $G$. Since the class of co-planar graphs is a subclass of $I_5$-free graphs all greedy algorithms use at most $\frac{5}{2}χ (G)$ colors for co-planar $G$'s. We prove that, even in a smaller class, this is an almost tight bound.

Section:
Proceedings

We analyze on-line chain partitioning problem and its variants as a two-person game. One person (Spoiler) builds an on-line poset presenting one point at time. The other one (Algorithm) assigns new point to a chain. Kierstead gave a strategy for Algorithm showing that width w posets can be on-line chain partitioned into $\frac{{5}^{w-1}}{4}$ chains. Felsner proved that if Spoiler presents an upgrowing poset, i.e., each new point is maximal at the moment of its arrival then there is a strategy for Algorithm using at most $\binom{w+1}{2}$ chains and it is best possible. An adaptive variant of this problem allows Algorithm to assign to the new point a set of chains and than to remove some of them (but not all) while covering next points. Felsner stated a hypothesis that in on-line adaptive chain covering of upgrowing posets Algorithm may use smaller number of chains than in non-adaptive version. In this paper we provide an argument suggesting that it is true. We present a class of upgrowing posets in which Spoiler has a strategy forcing Algorithm to use at least $\binom{w+1}{2}$ chains (in non-adaptive version) and Algorithm has a strategy using at most $O(w\sqrt{w})$ chains in adaptive version.

Section:
Proceedings

We consider the problem of solving a system of polynomial equations over fixed algebra $A$ which we call MPolSat($A$). We restrict ourselves to unary algebras and give a partial characterization of complexity of MPolSat($A$). We isolate a preorder $P(A)$ to show that when $A$ has at most 3 elements then MPolSat($A$) is in $P$ when width of $P(A)$ is at most 2 and is NP-complete otherwise. We show also that if $P ≠ NP$ then the class of unary algebras solvable in polynomial time is not closed under homomorphic images.

Section:
Proceedings

We examine how we can define several probability distributions on the set of Boolean functions on a fixed number of variables, starting from a representation of Boolean expressions by trees. Analytic tools give us a systematic way to prove the existence of probability distributions, the main challenge being the actual computation of the distributions. We finally consider the relations between the probability of a Boolean function and its complexity.

Section:
Proceedings