A proof theory for constructive default logic

In earlier papers we developed a constructive version of Reiter’s default logic; Constructive Default Logic (CDL) which is a default logic in which the fixed-point definition of extensions is replaced by a constructive definition. Constructive extensions have a computational advantage over Reiter’s extensions. Reiter’s default logic lacks a default proof theory for non-normal default rules, which was already observed by Reiter himself to be a weakness of his logic. In this paper we show that CDL does have a default proof theory.