The structure of chains in the optimal chain decomposition of a periodic schedule S is investigated. A finite oriented graph termed the Linis Graph (LG) is defined which serves as the key for this investigation. The edges of the LG are trip-types of S and…
In "A new implementation for applicative languages" Turner uses combinators to implement lambda expressions. This paper describes an experimental investigation of the efficiency of Turner's technique compared to more traditional reducers.
We prove a forgetful determinacy theorem saying that, for a wide class of infinitary games, one of the players has a winning strategy that is virtually memoryless: the player has to remember only bounded many bits of information. We use forgetful determinacy to give a…
Answering a question of Jeffrey Ullman, we prove that the problem in the title is shown to be undecidable.
A method of existential interpretation was introduced in [2]. It allows proving undecidability of modest strata of many first order theories. Here we improve the method and its presentation, strengthen somewhat the previous results and prove a couple of new results. The reader is not…
In the case of unbounded buffers, the negative answer follows from a result in [28].
Two small classes of first order formulae without function symbols but with identity, in prenex conjunctive normal form wit hall disjunctions binary, are shown to have a recursively unsolvable decision problem, whereas for another such class an algorithm is developed which solves the decision problem…
Papadimitriou and Yannakakis were interested whether Unique Sat is hard for {L - L' : L, L' are NP} when NP differs from co-NP (otherwise the answer is obvious). We show that this is true under one oracle and false under another.
In 1975 Annals of Mathematics Shelah interpreted true first-order arithmetic in the monadic theory of order under the assumption of the continuum hypothesis. The assumption is removed here.
The original problem was to find an algorithm deciding logical validity of sentences of the usual first-order logic.
I have long felt that, because it was posed as a cute problem about philosophers seated around a table, Dijkstra's dining philosopher's problem received much more attention than it deserves. (For example, it has probably received more attention in the theory community than the readers/writers…
During the late 70s and early 80s, Susan Owicki and I worked together quite a bit. We were even planning to write a book on concurrent program verification. But this paper is the only thing we ever wrote together. In [23], I had introduced a…
