ANNOTATED LOGIC REASONING BASED ON XML
Fuxi Zhu, Duanzhi Chen, Jia Rao
School of Computer, Wuhan University, Wuhan, China 430072
Keywords: Paraconsistent Logic, Annotate Logic, XML, Automatic Reasoning.
Abstract: Paraconsistent logic is able to handle the inconsistent knowledge reasonably. In this paper we propose using
XML as a tool to implement the presentation and reasoning of Annotation Logic--one of the paraconsitent
logic systems and investigate the problems about the automatic inference rules and inference strategies
under XML representation. Demonstrations are presented to show that XML can represent the Annotation
Logic conveniently and XML and its auxiliary tools can implement the inference mechanism efficiently.
1 INTRODUCTION
Inconsistency appears very often among the various
knowledge discovery systems in practice. The
knowledge which comes from different information
source may contradict each other. If the methods of
extraction of knowledge or the expression of
knowledge are inappropriate, or the knowledge is
beyond the validation scope, it will cause the
knowledge distortion or incompatibility. The most
simple situation is, if we obtain assertion A from
knowledge source s1, obtains assertion B from
information source s2, and obtain assertion ~A∨ ~B
from information source s3, that means A and B is
impossibly true at the same time. If these three
assertions are put together, then an inconsistence
occurs immediately.
It is not difficult to see that, as long as we extract
knowledge from the different sources, the
incompatibility processing is inevitable. But the
classical logic is nearly helpless to this kind of
incompatibility. For in classical logic, so long as the
contradiction exists in knowledge base, any
conclusion will be induced. Thus, a huge knowledge
base could be collapsed because of its containing a
small inconsistent subset. Therefore, the research in
this area has the great significance.
At present, the paraconsistent logic research is
being valued increasingly by logician and computer
scientists.
Brazilian logician da Costa proposed a set of
formal paraconsistent calculating system C(Da
Costa., 1992). The system C achieves the
paraconsistence by weakening the classical logic
deduction ability.
Following the idea of da costa, Kifer.M and
Subrahmanan.V.S put forward the Annotated
Logic(Kifer, M. 1992,).
M. Kifer and E. L. Lozinskii then further modify
the Annotated Logic system into APC (Annotated
Logic Calculus)( Kifer, M., Lozinskii, E.L. 1992).
In this article we take XML as a basic tool, and
implement the representation and the reasoning of
Annotated Logic
2 REPRESENT THE ANNOTATED
LOGIC WITH XML
The Annotated Logic is one of mature paraconsistent
logic formal systems. This logic introduces a set of
annotated truth values(context) τ in the language L.
If φ is a formula of language L and λ is a annotated
truth value, then φ:λ is a annotated formula. In the
Annotated Logic, it further t limits τ as a standard
complete lattice. For example, set τ=Four= {t, F, Τ ,
⊥ }. In this lattice, t and f stand for “true” and
“false”; Τ stands for “contradiction”; ⊥ stands for
“unknown”. O, classical two-value logic is the
specific case of the Annotated Logic.
Definition 1 If A is an atom formula and u ∈ τ,
then:
（1）A:u is an annotated atom.
（2）～…～(A:u) is called the k order mega-
literal, k means the symbol ~ appear k times.
229
Zhu F., Chen D. and Rao J. (2006).
ANNOTATED LOGIC REASONING BASED ON XML.
In Proceedings of WEBIST 2006 - Second International Conference on Web Information Systems and Technologies - Internet Technology / Web
Interface and Applications, pages 229-233
DOI: 10.5220/0001241702290233
Copyright
c
SciTePress
Definition 2 Suppose A
0
, A
1
…A
n
are the headers of a
literal, λ
0
, λ
1
, …, λ
n
are annotated values. A mega-
clause is a formula in the following form：
(
∀
x
1
) … (
∀
x
n
)A
0
:λ
0
∨ A
1
:λ
1
∨ …∨ A
n
:λ
n
Where, x
1
, x
2
… x
n
are variables appeared in A
i
; A
i
:λ
i
is a mega-literal whose order is smaller than or equal
to 1.
Because the XML language has strong capability
of semantics expression, we use XML to implement
the representation and reasoning of Annotated
Logic. For annotated literal φ:λ, its full expression
is:
sign predicate_name(argument_list):value
With the XML language, it can be express as
<annotated_predicate>
<predicate_sign> sign </predicate_sign>
<predicate_name> name </predicate_name>
<argument_list>
<argument>arg1</argument>
<argument>arg2</argument>
……
</argument_list>
<annotated_value> val </annotated_value>
</annotated_predicate>
In the section above, val belongs to Four = {t, f, Τ ,
⊥ }.
The mega-clause that defined in Definition 2 is
easily expressed with XML as:
<annotated_clause>
<annotated_predicate>
…
</annotated_predicate>
<annotated_predicate>
…
</annotated_predicate>
…
</annotated_clause>
A paraconsistent knowledge base under
Annotated Logic composes of many mega-clauses.
Thus it can be defined with XML as:
<knowledge_base>
<annotated_clause>
…
</annotated_predicate>
<annotated_clause>
…
</annotated_clause>
…
</knowledge_base>
So, a XML document can express a paraconsistent
knowledge base. To standardize the expression of
the parameters of a mega-literal, mega-clause and
the knowledge base, we use XML schema to define
XML document that represent a knowledge base.
Thus we can implement the various inference
mechanisms on this knowledge base.
3 THE AUTOMATIC REASONING
OF ANNOTATED LOGIC WITH
THE XML EXPRESSION
The conception of unifying also exists in the process
of refutation between the formulae of Annotated
Logic. It is similar to the unifying of the formulae of
the classical predicate logic. Under the expression of
XML, the selection process of parent clauses can be
implemented as the process of search and matching
in the XML document. Thus, we will discuss the
inference mechanism of Annotated Logic and how
to implement it.
Definition 3 set C
1
and C
2
are mega-clauses as
following:
C
1
≡(L
1
∨ …∨ L
i
∨ …∨ L
n
)
C
2
≡( L
1
′∨ …∨ L
j
′∨ …∨ L
m
′)
Where L
i
=(A:u), L
j
′=～(A′:ρ), A and A′ are able to
unify via a mgu θ, u, p∈ τ and p ≦ u, thus the
resolvent of refutation C
1
to C
2
via mega-literal L
i
and L’
j
can be defined as:
(L
1
∨ … ∨ L
i-1
∨ L
i+1
…L
n
∨ L
1
’ ∨ … ∨ L
j-1
’ ∨
L
j+1
’∨ …∨ L’
m
)θ
Where θ is called unifier of mega-refutation step, L
i
and L’
j
are mega-literals which are deleted at mega-
refutation step.
In Definition 3, it requires that the relation
between the annotated value u of 0 order literal and
the annotated value p of 1 order literal satisfies p≦
u.
For a set of mega-clauses S, a series of mega-
refutations between the mega-clauses of S and the
results of a mega-refutation are called a mega-
inference.
To realize mega-inference, Java package JDom
is used to parse the XML document which contains
the expression of the set of mega-clauses and to
produce the Document object, and then the
getChildren(“mega-clause”) method of the root
Document object is called to extract all the mega-
clauses from the knowledge base. These mega-
clauses constitute the initiative mega-clause set. Its
structure is a List. The target clauses which we want
to deduce is also in this List. The inference process
is just using the get(int i) method of the List to select
a clause from the set of mega-clause.
WEBIST 2006 - INTERNET TECHNOLOGY
230
It must be noted that the mega-refutation do not
possess the completeness. The following case is an
example to illustrate the incompleteness of mega-
refutation.
Example 1 set S={ p:t, p:f, ～ (p:Τ )}, S has no
model. But its mega-inference of null clause □ from
S does not exist. For Τ ≧ f and Τ ≧ t, ～(p:Τ )
can not refute with neither p:t nor p:f.
This example told us that, to ensure the
completeness of mega-inference, we have to
continue to prefect the inference mechanism.
Definition 4 Suppose u,u
1
,u
2
∈ τ, if u=∪ {u
1
,u
2
}, i.e.,
u is the least upper bound of u
1
and u
2
, the pair (u
1
,
u
2
) is called disassembly of u. (u
1
, u
2
) is called a
strict disassembly of u if (u
1
, u
2
) is a disassembly of
u, and u, u
1
, u
2
satisfy u
1
≠u≠u
2
.
In complete lattice Four, the strict disassembly of
truth Τ are pair (t, f) and pair (f, t). Whereas t, f and
⊥ have no disassembly.
It is not difficult to proof the following
predication.
Proposition 1 suppose A is a atom, C and D are
mega-clauses and u ∈ τ, (u
1
, u
2
) is a disassembly of
u, then:
(1) ╞(A:u
⇔ (A:u
1
＆A:u
2
)) and
(2) ╞(C∨～(A:u) ∨ D)
⇔ (C∨～(A:u
1
)∨～
(A:u
2
)∨ D)
Considering Proposition 1 and the fact that only
Τ can be disassembled in lattice Four, we further
extend the Definition 3 and put forward the
following definition.
Definition 5 Suppose C
1
and C
2
are the mega-
clauses in Definition 3, L
i
=(A:u), L
j
’=～(A’:p), u∈
{t, f}, p=Τ , and A, A′ can unify via mgu θ, then the
binary mega-refutation C
1
to C
2
over mega-literal L
i
and L’
j
can be defined as:
(L
1
∨ …∨ L
i-1
∨ L
i+1
…L
n
∨ L
1
’∨ …∨ L
j-1
’∨～
(A:﹁u)∨ L
j+1
’∨ …∨ L’
m
)θ
The purport of Definition 5 is to reduce some
unnecessary steps of disassembly. Because of L
j
’=～
(A’:Τ )
⇔ (～(A’:f)∨～(A’:t)), it can refute with
(A:t) or (A:f). The resolvent is ～(A:f)θ or ～(A:t)θ.
Hence, when two mega-clauses, one contains literal
L
i
=(A:t) or L
i
=(A:f) and the other contains literal
L
j
’=～(A’:Τ ), it can refute directly and no need to
disassemble ～(A’:Τ ) and then to do refute.
Definition 6 set D≡(D
1
∨ A
i
:u
i
∨ D
2
∨ A
j
:u
j
∨ D
3
), D
1
,
D
2
, D
3
are mega-clauses. If A
i
can unify with A
j
via
mgu θ and u
i
≦ u
j
, D’≡(D
1
∨ A
i
:u
i
∨ D
2
∨ D
3
)θ is
called the factor of D.
Similarly, set E≡D
1
∨～(A
i
:u
i
)∨ D
2
∨～(A
j
:u
j
)∨
D
3
is a mega-clause, if A
i
can unify with A
j
via mgu
θ and u
i
≦ u
j
, D”≡(D
1
∨ D
2
∨～(A
j
:u
j
)∨ D
3
)θ is also
called the factor of E.
As we saw above, there are two cases of
definition of factor. One case is positive literal being
merged and the other case is negative literal being
merged. In the clause corresponding to the factor D’,
A
i
, A
j
are positive literal and u
i
≦ u
j
. It indeed deletes
the literal containing u
j,
and A
i
:u
i
is reserved in D’.
In the clause corresponding to the factor D”, ～A
i
:u
i
and ～ A
j
:u
j
are mega-literal, u
i
≦ u
j
, the literal
containing u
i
is deleted, and ～A
j
:u
j
is reserved in
D”.
According to the Definition 6, we could leave
out unnecessary mega-literals. For example, in ～
(A
i
:t )∨～(A
j
: Τ ), we can leave out ～(A
i
:t).
Proposition 2 If C and D are mega-clauses and D is
a factor of C, C╞D. C╞D represents that D is the
logic conclusion of C, i.e., any model of C is also the
model of D.
Definition7 (subsumption ) suppose C
1
and C
2
are
mega-clauses in the following form：
C
1
≡A
1
:u
1
∨ …∨ A
n
:u
n
∨～(B
1
:ρ
1
)∨ …∨ (B
m
:ρ
m
)
C
2
≡G
1
:ψ
1
∨ … ∨ G
r
:ψ
r
∨～(H1:φ
1
) ∨ … ∨～
(H
s
:φ
s
)
C
1
subsumes C
2
if and only if exist a substitution θ
,
so as to:
(1) For all i, 1≤i≤n, exists j, 1≤j≤r, makes G
j
=A
i
θ
and u
i
≦ ψ
j
.
(2) For all l, 1≤l≤m, exists w, 1≤w≤s, makes
H
w
=B
l
θ and φ
w
≦ ρ
l
.
The requirement of the Definition of
subsumption is very strict. Mega-clause C
1
subsumeing C
2
requires that for all mega-literal A
i
:u
i
of C
1
, we must find a mega-literal G
j
:ψ
j
in C
2
and a
substitution θ make G
j
=A
i
θ and the annotated value
of G
j
satisfy u
i
≦ ψ
j
. Furthermore, for the mega-
literal of C
2
, the definition has the similar
requirement. We need to find a mega-literal H
w
:φ
w
ANNOTATED LOGIC REASONING BASED ON XML
231
in C
2
and the substitution θ make H
w
=B
l
θ and the
annotated value of H
w
satisfy φ
w
≦ ρ
l
.
Proposition 3 If C
1
and C
2
are mega-clauses and C
1
subsumes C
2
, then C
1
╞C
2
.
The advantage the definition 7 and proposition 3
bringing to us is that we can delete the mega-clause
in the process of mega-refutation. This action greatly
reduces the size of List which contains the XML
expression of the set of mega-clauses. If one more
mega-clause is added the List, it may nearly double
the size of List in the mega-refutation process.
Definition 8 set c
1
and c
2
are mega-clauses, then
mega-clause C is called a paraconsistent
refutation(p-refutation for short) if and only if C
is a
binary mega-refutation of C’
1
to C’
2
, where C’
i
(i=1,2)
are：
1) C
i
or
2) the factor of C
i
or
3) a mega-clause in C”
i
, C”
i
is disassembly of
C
i
.
It is not difficult to make out that the Definition
8 comprises the meaning of Definition 5, 6. In the
process of refutation, the factor is easy to get when
extracting the clause from the List. If a disassembly
is needed in step (3), the refutation can be finished
according to Definition 5.
Definition 9 An linear inference sequence C
1
, C
2
…
C
n
from the mega-clause set S, satisfy:
1) C
1
∈ S and
2) for i＞0, C
{i+1}
is one of p-refutation C
i
to C.
Inference sequence C
1
, C
2
… C
n,
is a para-
inference of S if and only if C
n
=□, where □ is null
clause or any clause in the following form:
(～(A
1
:⊥ )∨ …∨～(A
i
:⊥ ))
The proof of completeness of para-inference in
Definition 9 is similar to the proof of lifting-lemmas
of first order predicate logic. This implement
strategy of para-inference is also similar to the
support set strategy of first order predicate logic. In
the implement process, the selection of clauses from
the clause set is to call the get(int i) method of List.
The implementation of the unifying algorithm of two
mega-literals is to call get method of XML Element
and compare variable of the two literals one by one.
In this process the Xpath technology is used to get
all the variables and XLST technology is used to
realize the substitution of variables. Xpath is also
used to access the annotated value. Xpointer
technology is used for the matching of parameters
and locating the level of the sub-elements.
4 AN EXAMPLE OF REASONING
Take the medicine expert system as an example of
paraconsistent reasoning, we construct a medicine
expert system by consulting doctors. We suppose
that doctor A provides us the following three rules
(S
i
represents a symptom, D
i
represents a disease):
C
1
: D
1
(x):t∨ D
2
(x):t∨～(S
1
(x):t)∨～(S
2
(x):f)
C
2
: D
1
(x):f∨～(D
2
(x):t)
C
3
: D
2
(x):f∨～(D
1
(x):t)
Intuitively, this doctor tells us if one person is
inspected have symptom S
1
, and no symptom S
2
, and
then this patient suffers disease D
1
or disease D
2
.
Moreover, it tells us that no body suffers disease D
1
or disease D
2
simultaneity.
The information which Doctor B provides
expressed with mega-clauses is as following:
C
4
: D
1
(x):t∨～(S
2
(x):f)∨～(S
3
(x):t)
C
5
: D
2
(x):f∨～(S
3
(x):f)
Now, a pathology doctor examines the patients
Tom and Tim and describes the symptoms as
following:
C
6
: S
1
(Tom):t
C
7
: S
1
(Tim):t
C
8
: S
2
(Tom):f
C
9
: S
2
(Tim ):f
C
10
: S
3
(Tom):t
The pathology doctor's above report tells us that
Tom has the symptom S
1
, S
3
, but does not has the
symptom S
2
; Tom has the symptom S
1
but does not
has the symptom S
2.
Base on these examination results, it is easy for
us to prove that D
1
(Tom):t is a logic conclusion of
the set of mega-clause {C
1
, …, C
10
}. The p-
refutation of {C
1
,…, C
10
} ∪ { ～ D
1
(Tom ):t} is
shown as following:
E
1
:～(D
1
(Tom ):t) (initial inquiry)
E
2
:～(S
2
(Tom ):f)∨～S
3
(Tom ):t
(resolvent of E
1
and C
1
)
E
3
:～(S
3
(Tom):t) (resolvent of E
2
and C
8
)
E
4
: (resolvent of E
3
and C
10
)
Similarly, D
2
(Tom):f is also a logic conclusion of
{C
1
, …, C
10
}. The p-refutation of {C
1
, …, C
10
}∪
{D
2
(Tom):f} is shown as following:
E
1
:～(D
2
(Tom ):f) (initial inquiry)
F
2
:～(D
1
(Tom ):t) (F
1
and C
3
)
The rest part of the p-refutation is the same as the
steps from E
1
to E
4
WEBIST 2006 - INTERNET TECHNOLOGY
232
Until now, all the knowledge of these inquiries
involved is consistent. Now suppose that a third
doctor has already provided the following
information to us:
C
11
:D
2
(x):t∨～(S
3
(x):t)
Put the rules and “datum” that these three doctors
and pathology doctor provides together, when
inconsistence is needed to process. Because using
the rules Doctor 3 provides and data pathology
doctor provides may infer that Tom suffers disease
D
2
. Similarly, from the data Doctor 2 provides and
rules pathology doctor provides we can infer that
Tom suffers disease D
1
. Thus, Tom suffers both
disease D1 and disease D2. Therefore, when the rule
C
11
in knowledge base is considered, it can infer out
D
1
(Tom):Τ. The steps of mega-inference of ～
(D
1
(Tom ):Τ) are as following:
G
1
: ～(D
1
(Tom):Τ) (initial inquiry)
G
2
:～(S
2
(Tom):f)∨～S
3
(Tom):t∨～
(D
1
(Tom ):f) (Decomposes of C
4
and G
1
)
G
3
: ～(S
3
(Tom):t)∨～(D
1
(Tom):f)
(resolvent of G
2
and C
8
)
G
4
: ～(D
1
(Tom):f) (resolvent of G
3
and C
10
)
G
5
: ～(D
2
(Tom ):t) (resolvent of G
4
and C
2
)
G
6
: ～(S
3
(Tom ):t) (resolvent of G
5
and C
11
)
G
7
: (resolvent of G
6
and C
10
)
5 CONCLUSIONS AND FURTHER
WORKS
In this paper, we investigate how to use XML to
realize automatic reasoning of paraconsistent logic.
As we know, it is easy to produce the inconsistence
from knowledge discovery in WEB environment.
Therefore it is an appropriate way to express and
deal with coordinated logic. At present, XML is
more and more popular in the WWW community, so
using XML as a tool of Web knowledge discovery
and the expression of incompatible knowledge is a
very natural way.
In this paper, the prefect match of XML and Java
is subtly used to realize the inference mechanism of
Annotated Logic. In our implementation, the logic
truth is limited on Lattice Four. Under the complete
Lattice Four, the frame of Annotated logic was
modified and inference rule is reconstructed. This
modification does not lose the completeness. In the
implementation of the reasoning system, Java Jdom
package is used to parse and process the XML
document, in which inconsistent knowledge is
represented. Seeing from the process of knowledge
acquirement and knowledge inference, the
knowledge representation based on XML and with
the help of Java Jdom has a sound readability and
good efficiency of reasoning. It is a big step to made
paraconsistent reasoning from theory towards
practical application.
Our further research may concentrate on whether
the automatic reasoning theory that under the
classical logic come into existence under the
Annotated Logic. For example, besides most basic
binary mega-refutation, whether the hyper-
refutation, negative hyper-refutation, unit-refutation
and equality refutation inference mechanism or the
strategy are applicable in Annotated Logic. If true,
whether XML is a suitable tool to implement these
inference mechanisms and strategies is also a
research topic. Furthermore, the soundness and
completeness of these mechanisms and strategies
should be discussed and investigated too.
REFERENCE
Da Costa, 1992. Automated Theorem Proving in
Paraconsistent Logic Theory and Implementation. In
10th Int. Conf. on Automated Deduction. pp: 72-86.
Kifer, M., Subrahmanian, V. S. 1992. Theory of
Generalized Annotated Logic Programming and its
Applications. In Journal of Logic Programming,
12(4):335-368.
Kifer, M., Lozinskii, E.L., 1992. A Logic for Reasoning
with Inconsistency. IN Journal of Automated
Reasoning, 9(2): 179-215.
Gui, Q.Q., Chen, Z.L., Zhu, F.X., 2002. Paraconsisten
Logic and Artificial Intelligence, The press of Wuhan
University.
Zhu, F. X., Liu, L. P., Fu, J.M. 1998. Automatic
Reasoning in Paraconsisten Logic, In J. of Wuhan
University(Science Edition) 581
～
594.
ANNOTATED LOGIC REASONING BASED ON XML
233
