In the early 1920s, Pavel Urysohn proved his famous lemma (sometimes referred to as "first non-trivial result of point set topology"). Among other applications, this lemm...
In this note we consider the following decision problems. Let be a fixed first-order signature. (i) Given a first-order theory or ground theory T over of Turing degree , a program...
Many natural problems in computer science concern structures like graphs where elements are not inherently ordered. In contrast, Turing machines and other common models of computa...
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, als...
Over the past two decades, Gurevich and his colleagues have developed axiomatic foundations for the notion of algorithm, be it classical, interactive, or parallel, and formalized t...
Abstract. We describe our progress building the program ReductionFinder, which uses off-the-shelf SAT solvers together with the Cmodels system to automatically search for reduction...
Stable models of logic programs have been studied by many researchers, mainly because of their role in the foundations of answer set programming. This is a review of some of the de...
The question of whether there is a logic that captures polynomial time was formulated by Yuri Gurevich in 1988. It is still wide open and regarded as one of the main open problems...