Dual tableaux were introduced by Rasiowa and Sikorski (1960) as a cut free deduction system for classical first-order logic. In the current paper, a sound and complete proof procedure based on dual tableaux is proposed for

R₃

which is the standard Kleene logic augmented with a weak negation connective and an implication connective proposed, in another context, by Shepherdson (1989).

R₃

is used as a basis for defining Kleene Answer Set Programs (

ASP^K

programs). The semantics for

ASP^K

programs is based on strongly supported models. Both entailment procedures and model generation procedures for normal and non-normal

ASP^K

programs are proposed based on the use of dual tableaux and a model filtering technique. The dual tableau proof procedure extended with a model filtering technique is shown to be sound and complete for

ASP^K

programs, both normal and non-normal. Since there is a direct relationship between answer sets for classical ASP programs and

R₃

models for

ASP^K

programs, it can be shown that the sound and complete dual tableaux proof procedure with filtering for ASPK" role="presentation">ASPKprograms is also sound and complete for classical normal ASP programs. For classical non-normal ASP programs, the proof procedure is only sound, since an alternative semantics for disjunction is used in

ASP^K