Rational agents have to deal with internal and external inconsistencies. In this work we provide motivation, a language, a semantics, and procedures for reasoning logically in the face of contradiction. Our knowledge representation language is extended constraint logic programming under a generalization of wellfounded semantics with explicit negation, namely paraconsistent wellfounded semantics with explicit negation (or WFSXp for short). It comprises two forms of negation, default and explicit, and both the propositional and first-order cases are detailedly examined. An in-depth study of the semantics is provided with extensive comparisons to the relevant work in the literature. Besides the all important semantical issues, half of the work is dedicated to the procedural aspects of the language and semantics. As a result, the definition of a sound and theoretically complete goal-oriented proof procedure for the non-ground case is achieved, incorporating constructive negation methods, tabulation, and constraints. To the best of our knowledge, this the first time that such a procedure with such characteristics is advanced for wellfounded based semantics. Since WFSXp is a generalization of wellfounded semantics, the proof procedure is applicable to the latter. The more important implementation details are also discussed. All results and concepts are fully explained, exemplified, and proved.

In this small chapter, we start by making a short historic overview of the evolution of the semantics of normal and extended logic programs. Subsequently, we motivate the need for paraconsistent semantics for knowledge representation.

The chapter starts by presenting the language of (propositional) extended logic programs and associated terminology. Afterwards, we recall the several definitions of paraconsistent wellfounded semantics with explicit negation (or WFSXp for short) and prove their equivalence. A new alternating fixpoint definition of WFSXp is also given. The semantics' definition is completed with a model theory based on a truth-functional nine-valued logic. Finally, an embedding of our semantics into wellfounded semantics is studied.

This chapter provides extensive comparisons with several existing semantics dealing with paraconsistency. All semantics are briefly defined and explained. The main result is that most of these semantics are embeddable into WFS through appropriate and intuitive program transformations. Other related paraconsistent formalisms are concisely reviewed. We believe a good coverage of the topic as it stands has been attained. This highlights the central position that WFSXp occupies as a theory of paraconsistent extended logic programming.

In this chapter we address the issue of the syntactical asymmetry of logic programs: can one allow default negated literals in the heads ?

Here we examine two possible readings for default negation in the heads,and show how they are captured by WFSXp through the use of suitable program transformations without such occurrences, and thus not requiring any new fixpoint semantics. Furthermore, we extensively compare the three existing approaches in the literature to our own.

This chapter contains an in-depth examination of well-known strong and weak semantical properties, with respect to WFSXp and WFSXgp. Since these properties were defined for normal logic programming semantics, they do not immediately carry over for the extended paraconsistent case. Consequently, some of them were reformulated so as to encompass this more general setting. Other, specific, properties of both semantics are explored.

We augment the language of extended programs by adding variables and constraints to them. The definition of paraconsistent wellfounded model is enlarged to cope with this more general syntax, requiring new concepts. We start by giving meaning to these programs via the ground semantics defined in Chapter 2. A non-ground semantics is then studied and proved equivalent to the ground one. We also briefly discuss the treatment of more general classes of constraint theories.

We commence the study of the algorithmic part of $WFSX_p$ with a query-answering procedure for ground programs. We provide a top-down AND-tree characterization of the procedure, and prove its correctness with respect to our semantics. The rest of the chapter is devoted to the study of SLDNF-like proof procedures, with emphasis on termination issues. A complete characterization for the case of finite ground programs is given. The theory is accompanied with several illustrative examples. In Chapter 8 we generalize to non-ground programs.

In this chapter we provide a goal-oriented procedure which is sound and complete with respect to paraconsistent wellfounded semantics for constraint programs. For the first time an algorithm incorporates tabulation techniques, and constraint handling features (in particular constructive negation) for paraconsistent extended logic programs. Several illustrating examples are provided. In Chapter 10, this kernel algorithm will be improved with efficiency in mind.

In this chapter we prove soundness and completeness of SLX(D). Some additional results concerning the relationship between search trees in different forests are also presented.

In this chapter we address the main problems of a practical implementation of a constructive negation algorithm for WFSXp based on SLX(D). We outline a possible solution to the operational issues involved. The result is an efficient state-of-the-art query-answering procedure for extended logic programs. It subsumes SLG and SLGCN and is generally applicable. We advance informal justifications for the solutions proposed. No complex proofs are given and we will resort to the naturalness of the changes to SLX(D) for justifying their correctness preserving properties.

We single out the main conclusions from this work and point out future directions.