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
R3
which is the standard Kleene logic augmented with a weak negation connective and an implication connective proposed, in another context, by Shepherdson (1989).
R3
is used as a basis for defining Kleene Answer Set Programs (
ASPK
programs). The semantics for
ASPK
programs is based on strongly supported models. Both entailment procedures and model generation procedures for normal and non-normal
ASPK
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
ASPK
programs, both normal and non-normal. Since there is a direct relationship between answer sets for classical ASP programs and
R3
models for
ASPK
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
ASPK