It is known that paraconsistent logic programming, which is usually based upon a paraconsistent logic, is important in dealing with inconsistency-tolerant and non-monotonic reasoning appropriately. Firstly in this paper, a cut-free single succedent sequent system S_N4 and a cut-free multiple succedent sequent system M_N4 are introduced for Nelson's paraconsistent 4-valued logic N4, and the uniformity theorem (with respect to the notion of uniform proofs) which is established by Miller et al. is shown for S_N4 and M_N4. The framework using S_N4 provides us with an abstract paraconsistent logic programming language that can express inconsistency-tolerant reasoning and inexact information by using the properties of paraconsistency and constructible falsity. The framework using M_N4 gives an abstract paraconsistent disjunctive logic programming language that can allow to express disjunctive (indefinite) information in the program clauses. Secondly, a cut-free single succedent sequent system S_N16 is introduced for an extension N16 of N4, which is a variant of Shramko and Wansing's 16-valued logics, and the uniformity theorem for S_N16 is shown. The framework using S_N16 produces an abstract (extended) paraconsistent logic programming language that can also express a certain kind of synonymous information. Thirdly, a cut-free single succedent sequent system S_C is introduced for a fragment of Wansing's non-commutative logic COSPL, which is a non-commutative version of N4, and the uniformity theorem for S_C is shown. The framework using S_C provides us with an abstract paraconsistent ordered linear logic programming language that can represent both ordered and hierarchical information. The results of this paper are regarded as natural extensions of the results by Miller et al. and by Harland et al.
展开▼
