On termination of general logic programs w.R.T. constructive negation

AbstractThe notions of acyclicity and acceptability fail to characterize termination of general logic programs adequately under sldnf-resolution, as termination due to floundering is not captured. In this paper we establish the appropriate correspondence by considering sld-resolution with Chan's constructive negation. In particular, the resulting characterization provides a class of programs for which Chan's constructive negation is complete. Moreover, it can be used to formalize and implement problems in non-monotonic reasoning