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.

hdl.handle.net/1765/102045
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Tan, Y.-H. (1993). A proof theory for constructive default logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Retrieved from http://hdl.handle.net/1765/102045