Now showing items 62-81 of 100

    • On Distance Coloring 

      Kozen, Dexter; Sharp, Alexa (Cornell University, 2007-06-29)
      Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,2)-colorability is ...
    • On Hoare Logic and Kleene Algebra with Tests 

      Kozen, Dexter (Cornell University, 1998-12)
      We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary equational reasoning. It follows ...
    • On Hoare Logic, Kleene Algebra, and Types 

      Kozen, Dexter (Cornell University, 1999-07)
      We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus Hoare-style reasoning with ...
    • On Kleene Algebras and Closed Semirings 

      Kozen, Dexter (Cornell University, 1990-05)
      Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and analysis of algorithms. ...
    • On Moessner's Theorem 

      Kozen, Dexter; Silva, Alexandra (2011-06-12)
      Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^n, 2^n, 3^n, ... Paasche's theorem is a generalization of Moessner's; by ...
    • On Parallelism in Turing Machines 

      Kozen, Dexter (Cornell University, 1976-06)
      A model of parallel computation based on a generalization of nondeterminism in Turing machines is introduced. Complexity classes //T(n)-TIME, //L(n)-SPACE, //LOGSPACE, //PTIME, etc. are defined for these machines in a ...
    • On Regularity-Preserving Functions 

      Kozen, Dexter (Cornell University, 1995-11)
      We give a characterization of regularity-preserving functions.
    • On Teaching Left-Handed Children to Write 

      Kozen, Dexter (Cornell University, 1987-06)
      It is argued that the handwriting method commonly taught to left-handed children is incorrect and harmful. The disadvantages of this method are noted, and a new method alleviating these disadvantages is proposed.
    • On the Coalgebraic Theory of Kleene Algebra with Tests 

      Kozen, Dexter (2008-03-14)
      We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two open problems of Chen and ...
    • On the Completeness of Propositional Hoare Logic 

      Kozen, Dexter; Tiuryn, Jerzy (Cornell University, 1999-09)
      We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional ...
    • On the Complexity of Reasoning in Kleene Algebra 

      Kozen, Dexter (Cornell University, 1997-03)
      We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions $E$; that is, the complexity of deciding the validity of universal Horn formulas $E\imp ...
    • On the Complexity of the Horn Theory of REL 

      Hardin, Chris; Kozen, Dexter (Cornell University, 2003-05-08)
      We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.
    • On the Elimination of Hypotheses in Kleene Algebra with Tests 

      Hardin, Chris; Kozen, Dexter (Cornell University, 2002-10-21)
      The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used ...
    • On the Representation of Kleene Algebras with Tests 

      Kozen, Dexter (Cornell University, 2003-10-06)
      We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with star-continuity, are sufficient ...
    • On Two Letters versus Three 

      Kozen, Dexter (Cornell University, 2002-02-04)
      If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three ...
    • Optimal Coin Flipping 

      Kozen, Dexter (2009-06-02)
      This paper studies the problem of simulating a coin of arbitrary real bias q with a coin of arbitrary real bias p with minimum loss of entropy. We establish a lower bound that is strictly greater than the information-theoretic ...
    • Parallel Resultant Computation 

      Ierardi, Doug J.; Kozen, Dexter (Cornell University, 1990-01)
      A resultant is a purely algebraic criterion for determining when a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and sequential algorithms ...
    • Parikh's Theorem in Commutative Kleene Algebra 

      Hopkins, Mark; Kozen, Dexter (Cornell University, 1999-01)
      Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about least solutions of ...
    • Polynomial Decomposition Algorithms 

      Kozen, Dexter; Landau, Susan (Cornell University, 1986-08)
      In a recent paper [BZ], Barton and Zippel examine the question of when a polynomial $f(x)$ over a field of characteristic 0 has a nontrivial decomposition $f(x)=g(h(x))$. They give two exponential-time algorithms, both ...
    • Practical Coinduction 

      Kozen, Dexter; Silva, Alexandra (2012-11-11)
      Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes ...