N50 as an extension of G0 3

Abstract

We present an extension of GLukG, a logic that was introduced in [6] as a three-valued logic under the name of G03. GLukG is a paraconsistent logic de ned in terms of 15 axioms, which serves as the formalism to de ne the p-stable semantics of logic programming. We introduce a new axiomatic system, N-GLukG, a paraconsistent logic that possesses strong negation. We use the 5-valued logic N50 , which is a conservative extension of GLukG, to help us to prove that N-GLukG is an extension of GLukG. N-GLukG can be used as the formalism to de ne the p-stable semantics as well as the stable semantics.

Introduction

Deductive databases are an important aspect in the convergence of arti cial intelligence and databases [ 9 ]. Currently it is necessary to have complex reasoning tasks to deal with great amounts of data. Logic base systems are an option to provide such complex reasoning capabilities. Speci cally, Deductive Database Systems are forms of database management systems whose storage structures are designed around a logical model of data and at the same time inference modules for the Deductive Database Systems are designed on logic programming systems. The Deductive Database Systems are based on deductive database theories that always have associated a semantics. In general, a deductive database theory may give di erent answers to a query depending on the semantics used.

Two of the semantics that a database theory can be based on, are the stable logic programming semantics (stable semantics) as well as the p-stable logic programing semantics (p-stable semantics). The mathematical formalism to support those semantics is the theory of intermediate and paraconsistent logics; thus, intuitionism helps to express the stable semantics and the logic G03 helps to express the p-stable semantics. In this work we study a new paraconsistent logic called N-GLukG. N-GLukG has a stong negation besides having the native paraconsistent negation, and it is capable of expressing both, the p-stable and the stable semantics. With the help of the 5-valued logic N50 [ 5 ] we prove that N-GLukG is an extension of GLukG. Furthermore, N-GLukG can be used as the formalism to extend the p-stable semantics to a version that includes strong negation in a similar way as the stable semantics has been extended to include such a negation [ 4 ].

Our paper is structured as follows. In section 2, we summarize some de nitions and logics necessary to understand this paper. In section 3, we introduce a new logic that is an extension of a known logic, this new logic satis es a substitution theorem, and can express the stable semantics as well as the p-stable semantics. Finally, in section 4, we present some conclusions. 2

Background

We present several logics that are useful to de ne and study or logic N-GLukG. We assume that the reader has some familiarity with basic logic such as chapter one in [ 3 ]. 2.1

Hilbert style proof systems

One way of de ning a logic is by means of a set of axioms together with the inference rule of Modus Ponens.

As examples we o er two important logics de ned in terms of axioms, which are related to the logics we study later.

C! logic [ 2 ] is de ned by the following set of axioms:

Pos1 Pos2 Pos3 Pos4 Pos5 Pos6 Pos7 Pos8 C!1 C!2 a ! (b ! a) (a ! (b ! c)) ! ((a ! b) ! (a ! c)) a ^ b ! a a ^ b ! b a ! (b ! (a ^ b)) a ! (a _ b) b ! (a _ b) (a ! c) ! ((b ! c) ! (a _ b ! c)) a _ :a ::a ! a

The rst eight axioms of the list de ne positive logic. Note that these axioms somewhat constraint the meaning of the !, ^ and _ connectives to match our usual intuition. It is a well known result that in any logic satisfying axioms Pos1 and Pos2, and with modus ponens as its unique inference rule, the Deduction Theorem holds [ 3 ]. 2.2

Axiomatic de nition of GLukG

We present a Hilbert-style axiomatization of G03 that is a slight (equivalent) variant of the one presented in [ 6 ]. We present this logic, since it will be extended to a new logic called N-GLukG, which possesses a strong negation and is the main contribution of this work.

GLukG logic has four primitive logical connectives, namely GL := f!; ^; _; :g. GLukG-formulas are formulas built from these connectives in the standard form. We also have two de ned connectives: := ! (: ^ :: ).

$

:= ( ! ) ^ ( ! ).

GLukG Logic has all the axioms of C! logic plus the following:

E1 E2 E3 E4 E5 (: ! : ) $ (:: ! :: ) ::( ! ) $ (( ! ) ^ (:: ::( ^ ) $ (:: ^ :: ) ( ^ : ) ! ( ! ) ::( _ ) $ (:: _ :: )

! :: ))

Note that Classical logic is obtained from GLukG by adding to the list of axioms any of the following formulas: !:: ; !(: ! ); (: !: )!( ! ). On the other hand, ! : is a theorem in GLukG, that is why we call the \ " connective a strong negation.

In this paper we consider the standard substitution, here represented with the usual notation: '[ =p] will denote the formula that results from substituting the formula in place of the atom p, wherever it occurs in '. Recall the recursive de nition: if ' is atomic, then '[ =p] is when ' equals p, and ' otherwise. Inductively, if ' is a formula '1#'2, for any binary connective #. Then '[ =p] will be '1[ =p]#'2[ =p]. Finally, if ' is a formula of the form :'1, then '[ =p] is :'1[ =p]. 2.3

GLukG as a multi-valued logic and the multi-valued logic N50

It is very important for the purposes of this work to note that GLukG can also be presented as a multi-valued logic. Such presentation is given in [ 7 ], where GLukG is called G03. In this form it is de ned through a 3-valued logic with truth values in the domain D = f0; 1; 2g where 2 is the designated value. The evaluation functions of the logic connectives are then de ned as follows: x ^ y = min(x; y); x _ y = max(x; y); and the : and ! connectives are de ned according to the truth tables given in Table 1. We write j= to denote that the formula is a tautology, namely that evaluates to 2 (the designated value) for every valuation.

In this paper we keep the notation G03 to refer to the multi-valued logic just de ned, and we use the notation GLukG to refer to the Hilbert system de ned at the beginning of this section.

There is a small di erence between the de nitions of G03 and Godel logic G3: the truth value assigned to :1 is 0 in G3. G3 accepts an axiomatization that includes all of the axioms of intuitionistic logic. In particular, the formula (a ^ :a) ! b is a theorem, therefore G3 is not paraconsistent.

The next couple of results are facts we already know about the logic G03 Theorem 1. [ 6 ] For every formula , in GLukG. is a tautology in G03 i is a theorem Theorem 2 (Substitution theorem for G03-logic). [ 6 ]Let , and be GLukG-formulas and let p be an atom. If $ is a tautology in G03 then [ =p] $ [ =p] is a tautology in G03.

Corollary 1. [ 6 ]Let , and be GLukG-formulas and let p be an atom. If $ is a theorem in GLukG then [ =p] $ [ =p] is a theorem in GLukG.

Now we present N50 , a 5-valued logic de ned in [ 5 ]. We will use the set of values f 2; 1; 0; 1; 2g. Valid formulas evaluate to 2, the chosen designated value. The connectives ^ and _ correspond to the min and max functions in the usual way. For the other connectives, the associated truth tables are in table 2. In this section we introduce a new logic we will call N-GLukG. We prove that N-GLukG is an extension of GLukG (Theorem 4), that it satis es a substitution theorem (Theorem 5), and that it can express the stable semantics as well as the p-stable semantics. N-GLukG is de ned in terms of an axiomatic system. The axioms are chosen in such a way that N-GLukG is sound with respect to N50 , i.e. every theorem of N-GLukG is a tautology in N50 . The only inference rule is modus ponens. Here is our list of 19 axioms:

C!2 NPos1 NPos2 NPos3 NPos4 NPos5 NPos6 NPos7 NPos8 ::a ! a ::(a ! (b ! a)) ::((a ! (b ! c)) ! ((a ! b) ! (a ! c))) ::(a ^ b ! a) ::(a ^ b ! b) ::(a ! (b ! (a ^ b))) ::(a ! (a _ b)) ::(b ! (a _ b)) ::((a ! c) ! ((b ! c) ! (a _ b ! c))) ::(a _ :a) ::(::a ! a) ::((:a ! :b) $ (::b ! ::a)) ::(::(a ! b) ! ((a ! b) ^ (::a ! ::b))) ::( (a ! b) $ a^ b) ::( (a ^ b)$ a_ b) ::( (a _ b)$ a^ b) ::(a$ a) ::( :a $ ::a) ::( a ! :a)

We have a de ned connective: $ := ( ! ) ^ ( ! ). Also we note that the connective _ is not an abbreviation.

Observe that the inclusion of axiom C!2 assures that each of the other 16 axioms becomes a theorem in N-GLukG when dropping the double negation in front of them, this way we recover as theorems the axioms that de ne the positive logic as well as some of those that de ne GLukG. The convenience of having double negation in front of all these axioms is key in the proof of the substitution property (Theorem 5) presented at the end of this section. In particular the deduction theorem is valid in N-GLukG: ` if and only if ` ! .

Next we present some of the rst results about N-GLukG: Theorem 3. N-GLukG logic is sound with respect to N50 logic.

From this result we conclude that the logic N-GLukG is paraconsistent, since the formula (:a ^ a) ! b is not a theorem. Now we continue looking at some properties of N-GLukG. In particular we have that the connective of N-GLukG is not a paraconsistent negation as the following proposition shows.

Proposition 1. The formula (a^

a) ! b is a theorem in N-GLukG.

We also have the following result as a consecuence of theorem 3. Theorem 4. Every theorem in N-GLukG that can be expressed in the language of GLukG, is a theorem in GLukG.

Now we present a substitution theorem for N-GLukG logic. The next lemma is interesting on its own and plays a role in the proof of the theorem.

Lemma 1. If

N-GLukG.

is a theorem in N-GLukG, then :: is also a theorem in

For the next result, we introduce the notation formula ( $ ) ^ ( $ ). as equivalent to the Theorem 5. Let , and be N50 -formulas and let p be any atom. If , is a theorem in N-GLukG then [ =p] , [ =p] is a theorem in N-GLukG.

So far we have looked at some properties of logics N-GLukG and N50 . Now we would like to point out the theoretical value of these logics in the context of logic programming and knowledge representation.

Lemma 2. In N-GLukG the weak explosion principle is valid: For any formulas ; , the formula : ^ :: ! , is a theorem.

According to this, we can de ne a bottom particle in N-GLukG. De nition 1. For any xed formula : ^ :: . let us de ne the bottom particle ? as Lemma 3. The fragment of N-GLukG de ned by the symbols ^; _; !; ? contains all theorems of intuitionism.

As indicated in the introduction, logic GLukG(as some other paraconsistent logics) can be used as the formalism to de ne the p-stable semantics in the same way as intuitionism (as some other constructive logics) serves as the mathematical formalism of the theory of answer set programming (stable semantics) [ 8 ]. Accordingly we can state the next result.

Theorem 6. N-GLukG can express the stable semantics as well as the p-stable semantics. 4

Conclusions and Future Work

In this paper, we introduce a new logic called N-GLukG, it can be used as a formalism to de ne two logic programming semantics: stable and p-stable. These logic programming semantics could be used to de ne the semantics of deductive databases.

Funding. This work was supported by the Consejo Nacional de Ciencia y Tecnolog a [CB-2008-01 No.101581].

References

1. W. A. Carnielli , and J. Marcos . Logics of Formal Inconsistency. Handbook of Philosophical Logic , Kluwer Academic Publishers, pages 848 { 852 , 2001 .

2. N. da Costa . On the theory of inconsistent formal systems . Notre Dame Journal of Formal Logic , 15 ( 4 ): 497 { 510 , 1974 .

3. E. Mendelson . Introduction of Mathematical Logic . Wadsworth, Belmont, CA, third edition, 1987 .

4. M. Ortiz and M. Osorio . Strong Negation and Equivalence in the Safe Belief Semantics . In Journal of Logic and Computation , 499 - 515 , April, 2007 .

5. M. Osorio , C. Zepeda , J.L. Carballido et al. Mathematical Models and ITC: Theory and Applications. Chapter 1 : Mathematical Models . Section 2: N5 as an extension of G3. Fondo Editorial BUAP . ISBN: 978-607-487-353-5 . 1: 11 - 18 , 2011 .

6. M. Osorio and J. L. Carballido . Brief study of G'3 logic . Journal of Applied NonClassical Logic , 18 ( 4 ): 79 { 103 , 2008 .

7. M. Osorio , J. A. Navarro , J. Arrazola , and V. Borja . Logics with common weak completions . Journal of Logic and Computation , 16 ( 6 ): 867 { 890 , 2006 .

8. D. Pearce . Stable Inference as Intuitionistic Validity . The journal of Logic Programming , 38 : 79 - 91 , 1999 .

9. DLV system . http://www.dlvsystem.com/dlvdb/. (Last consulted: April 15 , 2013 .).