| Abstract. We show that the Mean Value Theorem is provable in the weak subsystem RCA0 of second order arithmetic. Note that it is impossible to prove in RCA0 that every continuous function on the interval [0,1] attains maximum and minimum values, and that the usual proof of the Mean Value Theorem makes use of this theorem. |
On the Elimination of Hypotheses in Kleene Algebra with Tests. Technical Report 2002-1879, Computer Science Department, Cornell University, October 2002 (with D. Kozen). postscript pdf
| Abstract. 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 to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron, 2000). |
On the Complexity of the Horn Theory of REL. Technical Report 2003-1896, Computer Science Department, Cornell University, May 2003 (with D. Kozen). postscript pdf
| Abstract. We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete. |
How the Location of * Influences Complexity in Kleene Algebra with Tests. In F. Baader and A. Voronkov, editors, Proc. 11th Int. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004), volume 3452 of Lecture Notes in Artificial Intelligence, pages 224-239, Montevideo, Uruguay, March 2005. Springer-Verlag. (This is the full version of the paper, with an appendix for proofs that do not appear in the conference proceedings.) postscript pdf
| Abstract. The universal Horn theory of relational Kleene algebra with tests is of practical interest, particularly for program semantics, where Horn formulas can be used to verify correctness of programs or compiler optimizations. Unfortunately, this theory is known to be Pi-1-1-complete. However, many formulas arising in practice fall into fragments of the theory that are of lower complexity. In this paper, we see that the location of occurrences of the Kleene asterate operator * within a formula has a great impact on complexity. Using syntactic criteria based on the location of *, we give a fragment of the theory that is Sigma-0-1-complete, and a slightly larger fragment that is Pi-0-2-complete. We show that the same results hold over *-continuous Kleene algebras with tests. The techniques exhibit a relationship between first-order logic and the Horn theories of relational and *-continuous Kleene algebra, even though the theories are not first-order axiomatizable. |
Proof Theory for Kleene Algebra. To be presented at LICS 2005 (Logic in Computer Science). postscript pdf
| Abstract. The universal Horn theory of relational Kleene algebra with tests (RKAT) is of practical interest, particularly for program semantics. We develop an (infinitary) proof system, based on well-founded trees of finite automata, which is sound and complete for this theory. A small modification of this system yields a proof system which is sound and complete for the universal Horn theory of *-continuous Kleene algebras with tests (KAT*). This sheds light on the relationship between RKAT and KAT*. |
Modularizing the Elimination of r=0 in Kleene Algebra. Submitted to Logical Methods in Computer Science. postscript pdf
| Abstract. Given a universal Horn formula of Kleene algebra of the form r=0 --> s=t, it is already known that we can efficiently construct an equation s'=t' which is valid if and only if r=0 --> s=t is valid. This is an example of elimination of hypotheses, which is useful because the equational theory of Kleene algebra is decidable while the universal Horn theory is not. We show that hypotheses of the form r=0 can still be eliminated in the presence of other hypotheses. This lets us extend any technique for eliminating hypotheses to include hypotheses of the form r=0. |
Last modified 20 Apr 2005.