Abstract :
Summary form only given, as follows. One award was made in 2015 to honor an outstanding paper from the IEEE Symposium on Logic in Computer Science 1995 held in San Diego, California, USA. It went to "Completeness of Kozen´s Axiomatisation of the Propositional μ-Calculus" by Igor Walukiewicz. The Award Committee was made up of Martin Grohe, Dexter Kozen, Dale Miller (chair), and Prasad Sistla. The propositional μ-calculus (now more commonly known as the modal μ-calculus) was first published in 1983 by D. Kozen, although the system had been studied much earlier by J. de Bakker and D. Scott (unpublished notes, 1969). The system subsumes many popular propositional logics of programs, including linear temporal logic, computation tree logic CTL*, and propositional dynamic logic. Kozen proposed a deductive system whose chief rule of inference was a variant of the fixpoint induction rule of D. Park and conjectured it to be complete. During the decade after its introduction, this calculus attracted a great deal of attention within computer science circles. Despite the attention given to this calculus, it was not until this paper by Walukiewicz a dozen years later that the proof system was finally shown to be complete. In order to prove the completeness theorem, several technical innovations were developed. A full version of this paper appeared in Information and Computation in 2000.
