Signed Dual Tableaux for Kleene Answer Set Programs

Abstract

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}_3$, which is the standard Kleene logic augmented with a weak negation connective and an implication connective proposed, in another context, by Shepherdson (1989). ${R}_3$ is used as a basis for defining Kleene Answer Set Programs ($\textsc {ASP}^{K}$programs). The semantics for $\textsc {ASP}^{K}$programs is based on strongly supported models. Both entailment procedures and model generation procedures for normal and non-normal $\textsc {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 $\textsc {ASP}^{K}$programs, both normal and non-normal. Since there is a direct relationship between answer sets for classical ASP programs and ${R}_3$ models for $\textsc {ASP}^{K}$programs, it can be shown that the sound and complete dual tableaux proof procedure with filtering for $\textsc {ASP}^{K}$programs 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 $\textsc {ASP}^{K}$.

This work is partially supported by the Swedish Research Council (VR) Linnaeus Center CADICS, the ELLIIT network organization for Information and Communication Technology, the Swedish Foundation for Strategic Research (SymbiCloud Project), and the Vinnova NFFP6 Project 2013-01206.