TELKOM
NIKA Indonesia
n
Journal of
Electrical En
gineering
Vol.12, No.7, July 201
4, pp
. 5567 ~ 55
7
4
DOI: 10.115
9
1
/telkomni
ka.
v
12i7.450
3
5567
Re
cei
v
ed Se
ptem
ber 26, 2013; Revi
se
d Jan
uary 6, 2014; Accept
ed Feb
r
ua
ry
2, 2014
Reduction on Propositional Logic Set Based on
Correlation Analysis
Zhi Huilai
Schoo
l of Com
puter Scie
nce
and T
e
chno
log
y
, He
nan Po
l
y
t
e
chn
i
c Univ
ersi
t
y
Jiaoz
uo He
na
n
P.R.China, +
8
6-03
91-3
9
8
7
7
1
1
email: zh
ihu
ila
i
@
12
6.com
A
b
st
r
a
ct
A know
le
dge
b
a
se is
red
u
n
d
a
n
t if it co
ntains
parts
that c
a
n
be
inferre
d fro
m
th
e rest
of it
. In this
pap
er, w
i
th n
o
district
bo
und,
w
e
study
the
reducti
on
t
heor
y an
d
alg
o
rith
m
on
pro
pos
iti
on
log
i
c s
e
t. T
h
e
prop
ositio
ns of
a given
prop
o
s
ition set fall
in
to three
categ
o
r
ies: necess
a
ry
propos
it
io
n, useful pro
pos
itio
n,
and
use
l
ess
propos
ition. A r
e
ductio
n
of a
gi
ven set is
co
mp
ose
d
of a
ll
the nec
essary prop
ositio
ns
a
n
d
some us
eful
p
r
opos
itions. At
the b
egi
nni
ng
w
e
introd
uce
ind
u
ced
for
m
al
context of pr
o
positi
on s
e
t, an
d
then pro
pos
e the metho
d
of reducti
on o
n
pr
opos
ition s
e
t based o
n
correl
a
tion a
n
a
l
ysis.
Ke
y
w
ords
: pro
positi
ona
l lo
gic
,
redund
ancy, forma
l co
ncept
ana
lysis, assoc
i
atio
n rules
Copy
right
©
2014 In
stitu
t
e o
f
Ad
van
ced
En
g
i
n
eerin
g and
Scien
ce. All
rig
h
t
s reser
ve
d
.
1. Introduc
tion
More and m
o
re available
kno
w
le
dge acq
u
isitio
n
ways
ma
ke knowl
edge
da
tabases
become mo
re and mo
re
compl
e
x, and then a dev
elopme
n
t bottleneck o
c
curs in kn
owl
e
d
ge
databa
se red
u
ction. Unlike
truth
maint
enan
ce sy
ste
m
[1] which is due to th
e
ability of these
s
y
s
t
e
m
s
to
r
e
s
t
or
e co
nsis
te
nc
y, k
now
le
dg
e
d
a
ta
base redu
cti
on i
s
the
transfo
rmatio
n
o
f
informatio
n in
to a corre
c
te
d, ord
e
re
d, a
nd si
mp
lified
form. A kn
owledge
ba
se i
s
red
unda
nt if it
contai
ns
so
me red
und
a
n
t parts, tha
t
is, it is
equivalent to one of its proper
su
bsets [2].
Gene
rali
zed,
the term redu
ndan
cy is d
e
fined a
s
by
th
e gene
ratio
n
of the sam
e
fact mo
re tha
n
once duri
ng the sam
e
prob
lem re
solutio
n
[3].
The p
r
o
b
lem
of re
dun
da
ncy may
be
either hig
h
l
y
importa
nce
of the
kn
o
w
led
ge it
expre
ss,
or
a mista
k
e
th
at ha
s b
een
made
in
th
e kno
w
ledg
e
ba
se. In
pa
rticula
r
, d
a
ta
base
update in
cre
a
se
s its si
ze
expone
ntially [4], and re
d
unda
ncy ma
kes this p
r
obl
e
m
worse. In any
expert
syste
m
, avoiding
redu
nda
ncy i
s
al
so
of
int
e
re
st in
real
-time syste
m
s for
whi
c
h t
he
inferen
c
e e
n
g
i
ne is time co
nsumi
ng [5].
Algorithm
s fo
r che
cki
ng
re
dund
an
cy of
kno
w
le
dge
b
a
se
s h
a
ve b
e
en devel
ope
d
for the
ca
se of prod
uction
rule
s [6]. Complexit
y
analysis o
n
Horn kn
owl
e
dge ba
se
s h
a
s be
en give
n in
two pape
rs [7] and [8]; Later, with no ot
her st
rict
bou
nds, de
cidin
g
whethe
r formula is mini
mal is
proved co
NP-hard
[9].
Red
und
ancy
elimination
is
relevant
to fo
rmula mi
nimization, an
d
ca
n be
con
s
ide
r
ed a
s
a
wea
k
form of
it. Redun
dan
cy eliminatio
n
has t
w
o
adv
antage
s, firstl
y it seems
so
meho
w ea
sie
r
to
remove redu
ndant cla
u
se
s, and se
co
n
d
ly it doesn’
t chan
ge the syntacti
c form of a knowl
edge
base [2].
Wheth
e
r
a
system can
g
i
ve an a
p
p
r
opriate
expla
nation
of inferential
a
s
well a
s
redu
ction p
r
o
c
e
ss i
s
an im
portant fa
ctor which
cu
sto
m
ers will take into accou
n
t
when cho
s
e
a
system, but this proble
m
h
a
s gai
ned little con
c
e
r
n.
Red
u
ct
io
n on
f
u
zzy
inf
e
ren
c
e r
u
le
s is al
so
studied, a
nd neu
ral n
e
twork [10], im
plicatio
n-
based m
odel
s a
nd
co
njun
ction-ba
sed
model
s [5] a
r
e ad
opted i
n
these
re
se
arches,
but all
th
ese
resea
r
che
s
gi
ve little hint o
n
the probl
em
discusse
d in this pap
er.
Formal
Con
c
ept Analysis
(FCA
) as a cat
egori
z
atio
n method aim
s
at grouping
obje
c
ts
descri
bed by
comm
on attri
butes. In this frame
w
ork,
a categ
o
ry is preci
s
ely define
d
as a maxim
a
l
set of o
b
je
cts sha
r
ing
a
maximal set
of attr
ibute
s
. Such
groupi
ngs
are then
gathe
red i
n
a
hiera
r
chi
c
al,
lattice-ba
s
e
d
structu
r
e whi
c
h strai
g
htforwa
r
dly exhibits
va
ri
ous rel
a
tion
ship
s
betwe
en
cate
gorie
s a
nd th
eir sub
-
and
sup
e
r-catego
ri
es. Be
ca
use
of its co
ncep
tual stru
ctu
r
e
to
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NI
KA
Vol. 12, No. 7, July 201
4: 5567 – 55
74
5568
facilitate the
developm
ent
and di
scu
ssi
o
n
, in a
se
n
s
e,
the co
ncept l
a
ttice ha
s b
e
c
ome
a me
a
n
s
for external reco
gnition d
e
c
ad
es [11].
FCA h
a
s be
en me
ntione
d in
pro
p
o
s
ition
set redu
ction [1
2], a
nd formal
co
ntext is
adop
eted to
depi
ct an
info
rmation
sy
ste
m
, but in
[12]
the te
chni
qu
e of
co
rreltai
o
n
an
alysi
s
i
s
no
t
use
d
. And fo
r this
rea
s
on
, without of correltai
on a
nalysi
s
it is i
m
posi
b
le to
point out wh
y a
formula i
s
red
unda
nt.
In this pap
er, we will u
s
e formal
con
t
ext to depict propo
sition
set, and p
r
opo
se a
redu
ction al
g
o
rithm ba
se
d on the tech
ni
que of co
rrela
t
ion analysi
s
.
2. Preliminaries
In this sectio
n, it is explain
ed some relat
i
ve con
c
ept
s
of this pap
er,
inclu
d
ing two-valued
prop
ositio
n lo
gic an
d forma
l
con
c
ept an
a
l
yais.
2.1. T
w
o
-
v
a
lued Proposition Logic
The fo
rmula
s
of propo
sitional
cal
c
ulu
s
, also
call
ed
pro
p
o
s
itiona
l formula
s
[1
3], are
ex
pre
ssi
on
s su
ch
a
s
((
)
)
A
BC
. Their definitio
n begin
s
with t
he arbitra
r
y choice of a set
of
prop
ositio
nal
variable
s
. Th
e alph
abet
co
nsi
s
ts of the l
e
tters i
n
along with th
e symbols fo
r th
e
prop
ositio
nal
con
n
e
c
tives and p
a
renth
e
se
s, all of
whi
c
h a
r
e a
s
sume
d to n
o
t
be in
. The
formulas will
be certain ex
pre
ssi
ons (that is, strings
of sy
mbols) over this alphabet.
Defini
tion 1.
Formul
as a
r
e
inductively d
e
fined a
s
follows:
(1) Ea
ch p
r
op
osition
a
l varia
b
le is, on its o
w
n, a formul
a
.
(2) If
is a formula, then
is a formula.
(3) If
and
a
r
e form
ula
s
, and
is any bi
nary conn
ecti
ve, then
is a
formula.
Her
e
coul
d b
e
(but is not li
mited to) the usu
a
l ope
rato
rs
,
,
, or
.
Defini
tion 2.
In p
r
op
ositio
nal lo
gic,
an
atomi
c
form
ula i
s
a
form
ula that
co
ntains no
logical co
nne
ctives.
Defini
tion 3.
A proof of a formal sy
stem is a finite formula
se
ries
12
,,
,
n
A
AA
, and
every
()
i
A
in
is eith
er a
axiom o
r
a re
sult in
du
ced
by usi
ng
MP based o
n
j
A
and
,
k
A
jk
i
.
Then the
seri
es is
calle
d a proof of
n
A
, and
n
A
is called a th
eore
m
and d
enoted a
s
n
A
.
Notation: Let
be a set of formulas a
nd
()
F
S
be the universe of all formul
as.
Defini
tion 4.
Ded
u
ctio
n of
is a finite fo
rmula
seri
es
12
,,
,
n
A
AA
, and
every
()
i
A
in
is eith
er
a axi
o
m o
r
a
re
sul
t
indu
ced
by
usin
g MP b
a
s
ed
on
j
A
an
d
,
k
A
jk
i
, then
n
A
is
call
dedu
ction, an
d
n
A
. A propositi
on
A
is red
und
ant if an only if
()
A
A
.
Notation:
{|
}
()
()
DA
F
S
A
.
Defini
tion 5.
Suppose a map
p
ing
v
:
{0
,
1
}
, if
()
(
)
vA
v
A
an
d
()
(
)
(
)
vA
B
v
A
v
B
hold
s
, then
v
is a homo
m
orp
h
ism of
type
(,
)
and calle
d
an
assignm
ent o
f
. Moreover,
()
vA
is call
ed an
assignm
ent o
f
A
, and all of the assig
n
me
nts of
forms an u
n
i
v
erse a
nd de
noted a
s
.
Defini
tion 6.
Suppo
se
A
, if for any a
s
sign
ment
v
and
()
1
vA
ho
ld
s
,
th
en
A
is
called
a ta
utology. Othe
rwi
s
e, if a
n
y assignm
ent
v
and
()
0
vA
hold
s
, th
en
A
is called a
contradi
ction.
Lemma 1.
Formula
A
is an a
x
iom of a formal system, if and only if
A
is a tautology.
Lemma 2.
Suppo
se
is a finite propo
si
tion set of
()
F
S
,
A
is a prop
osi
t
ion of
,
A
if and only if
A
is a tautology
respe
c
t to
.
2.2. Formal Conc
ept
An
aly
s
is
Before p
r
o
c
e
eding,
we b
r
i
e
fly recall the
FCA termino
l
ogy [14]. Given a fo
rmal
context
(,
,
)
K
GM
I
, where
G
is called a set of object
s,
M
is call
ed a
set of at
tributes,
and
the bi
nary
relation
IG
M
sp
ecifie
s the
relation
s bet
wee
n
o
b
ject
s a
nd
attrib
utes, two d
e
rivation
function
s
f
and
g
are define
d
for
A
G
and
BM
,
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
Red
u
ctio
n on
Propo
sitional
Logic Set Ba
sed o
n
Co
rrel
ation Analysi
s
(Zhi
Huilai
)
5569
()
{
|
:
}
f
Am
M
g
A
g
I
m
;
()
{
|
:
}
g
Bg
G
m
B
g
I
m
.
In words
,
()
f
A
is the set of attributes
comm
o
n
to all object
s
of
A
and
()
g
B
is the set
of object
s
sh
aring all attri
b
utes of
B
.
Both
((
)
)
g
fA
and
((
)
)
f
gB
are extensive,
idempote
n
t a
nd mon
o
tono
us a
nd the
r
e
f
ore
said to be
clo
s
ed.
A formal con
c
ept of the context
(,
,
)
K
GM
I
is a pair
(,
)
A
B
, where
A
G
,
BM
,
()
f
AB
and
()
g
BA
. The
s
e
t
A
is
calle
d the extent
and
B
is
call
ed the i
n
tent
of the
c
o
nc
ep
t
(,
)
A
B
.
A c
o
nc
ep
t
(,
)
A
B
is
a su
b-co
ncep
t of
(,
)
CD
if
A
C
(
e
qu
ivale
n
t
ly,
DB
), then
(,
)
CD
is a
supe
r-co
nce
p
t of
(,
)
A
B
. We write
(,
)
(
,
)
A
BC
D
and
de
fine the
relati
on
,
,
and
as
us
ual. If
(,
)
(
,
)
A
BC
D
and there is
no
(,
)
EF
such t
hat
(,
)
(,
)
(
,
)
EF
A
BC
D
, the
n
(,
)
A
B
is a
lowe
r neig
h
b
o
r of
(,
)
CD
and
(,
)
CD
is a uppe
r nei
g
hbor
of
(,
)
A
B
; notation,
(,
)
(
,
)
A
BC
D
and
(,
)
(
,
)
CD
A
B
.
The
set
of all
co
ncepts o
r
d
e
red
by
form
s a
lattice,
which
is de
not
ed by
()
LK
a
nd i
s
calle
d the
co
nce
p
t lattice
of the contex
t
K
. The relation
defines th
e edg
es in th
e cove
rin
g
grap
h of
()
LK
.
Defini
tion 7.
Let
(,
)
CA
B
be a given co
ncept, if
RB
sat
i
sf
ie
s
()
()
g
Rg
B
A
an
d
for any
TR
, we hav
e
()
(
)
g
Tg
R
, then
R
is said to be a i
n
tent redu
ctio
n of
C
[15, 16].
Rem
a
r
k
.
Suppose the intent r
edu
ction of con
c
ept
(,
)
CA
B
is
R
,
then we ca
n get a
n
asso
ciation
rule [17]
()
RB
R
. The me
aning
of
the
rule
is:
i
f
R
c
a
n re
pr
es
en
t c
o
n
c
e
p
t
C
,
then the othe
r attribute
s
of
C
can be d
e
riv
ed from
R
.
Example 1.
Give a
form
al
co
ntext
K
, and its corre
s
po
nding
con
c
ep
t lattice i
s
sh
own
in
Figure 1.
Table1. Fo
rm
al Context
a b c
d e f
g
1
2
3
4
5
6
7
23
57
cg
#6
a
b
cdef
g
#9
23
5
a
b
c
e
g
#8
12
35
a
c
#5
6
b
cdef
#7
235
6
b
ce
#4
12
35
6
7
c
#3
123
45
67
#1
23
45
6
b
e
#2
Figure 1.
()
LK
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NI
KA
Vol. 12, No. 7, July 201
4: 5567 – 55
74
5570
For exam
ple,
the intent re
ductio
n
of co
nce
p
t
({
2
,
3
,
5
,
6
}
,
{
,
,
}
)
bce
is
{,
}
bc
and
{,
}
ce
, so b
y
Definition 7 a
nd its rem
a
rk
we get a
s
soci
ation rule
s
bc
e
and
ce
b
.
3. Propositio
n Logic Set
Redu
ction
Based on F
C
A
A kno
w
led
ge
base is
re
dun
dant if it co
ntains
pa
rts tha
t
can
be infe
rred from the
rest
of
it. We assu
m
e
that the set
discu
s
sed i
n
this p
ape
r i
s
a
set with
o
u
t tautology, for tautologi
e
s
can be e
a
sily
checke
d an
d removed, a
nd thes
e d
o
n
’
t change the
complexity of the problem
s
c
o
ns
ide
r
ed
he
r
e
.
Not all th
e el
ement of
a gi
ven propo
siti
on set play
s t
he same
rol
e
, som
e
a
r
e n
e
c
e
s
sary,
while
some
a
r
e
un
wanted.
The
redu
ctio
n of
a p
r
op
osition set mu
st
en
su
re th
e
same
rea
s
o
n
in
g
ability after deleting unwanted formul
a.
Defini
tion 8.
Suppo
se
0
and
0
()
(
)
DD
, for
0
A
, if
0
()
(
)
DA
D
, th
en
0
is calle
d a re
ductio
n
of
an
d denote
d
as
re
d
.
Defini
tion 9.
Given a
p
r
op
osition
set
, and its redu
cti
on
set i
s
{(
)
|
}
re
d
t
tT
(
T
is t
h
e
index set), th
en the pro
p
o
s
ition of
falls
into three categories
:
a) Ne
ce
ssa
r
y propo
sition
A
:
()
re
d
t
tT
A
;
b) Useful p
r
o
positio
n
B
:
((
)
(
)
)
re
d
t
re
d
t
tT
tT
B
;
c) Usel
ess
p
r
opo
sition
C
:
((
)
)
red
t
tT
C
.
Notation: all the ne
cessa
r
y
propo
sition
s
form ne
ce
ssa
r
y prop
osition
set denoted
by
A
,
and all th
e u
s
eful p
r
op
osit
ions fo
rm u
s
eful pro
p
o
s
ition set den
oted by
B
, and al
l the usele
s
s
prop
ositio
ns f
o
rm u
s
ele
s
s prop
ositio
n set denoted by
C
.
Example 1.
Given a
prop
ositio
n
set
{,
,
}
ab
a
b
, it is
eas
y
to verify tha
t
{,
}
red
aa
b
or
{,
}
ab
, and the
r
efore
by Defi
nition 8
we
h
a
ve
{}
A
a
,
{,
}
B
ba
b
, and
C
(
denote
s
an
empty set
)
.
Let
12
,,
{}
,
n
A
AA
be an
two-val
ued
propo
sition
set
and
assu
me
it ha
s m
ato
m
ic
fo
r
m
u
l
as
, name
l
y,
12
,,
,
m
p
pp
.
Let
be the u
n
iverse
of all a
s
sign
ment of
, then
can
be
depi
cted by a
serie
s
of m-d
i
mensi
onal ve
ctors and
has
2
m
su
ch v
e
ct
o
r
s.
Define
a bin
a
r
y relatio
n
I
on
, for any
v
and
i
A
, we
have
i
vI
A
if and only
if
()
1
i
vA
. Then
(,
,
)
I
forms a
form
al
context, an
d
is
called
-ind
uce
d
formal
context. In
this formal
co
ntext, objects are the elem
ents of
, attributes are the e
l
ements of
.
Defini
tion 1
0
.
Suppo
se
()
F
S
, and
-indu
ce
d formal
cont
ext is
(,
,
)
KI
,
and defin
e two derivation f
unctio
n
f
and
g
on
P
and
Q
as foll
ows:
()
:
{
|
,
(
)
1
}
ii
fP
A
v
P
v
A
;
()
:
{
|
,
(
)
1
}
ii
gQ
v
A
Q
v
A
.
It is easy to prove that functions
f
and
g
form a Galois
co
nne
ction.
By computin
g
intent re
du
ction of
eve
r
y concept of formal context
(,
,
)
I
, we
can
get
all the
asso
ci
ation rule
s
which
tell the
correl
ation
s
b
e
twee
n p
r
op
osition
s
co
ntained
in
, and
denote all the
s
e a
s
soci
atio
n rule
s by set
R
.
Theorem 1.
In
formal
con
t
ext
(,
,
)
I
,
12
,
QQ
and
21
QQ
,
21
()
(
)
DQ
DQ
if and
only if
2
Q
is an i
n
tent redu
ctio
n of con
c
ept
11
((
)
,
)
g
QQ
.
Proof.
21
()
(
)
DQ
DQ
for any
()
A
FS
,
12
,
QA
Q
A
21
QQ
21
2
QQ
Q
.
A
cco
rdi
ng to Definition 7 a
nd its rema
rk, we can get that
2
Q
is an intent redu
ction
of conce
p
t
11
((
)
,
)
g
QQ
.
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
Red
u
ctio
n on
Propo
sitional
Logic Set Ba
sed o
n
Co
rrel
ation Analysi
s
(Zhi
Huilai
)
5571
Corollar
y
1.1.
In
formal context
(,
,
)
I
,
12
,
QQ
,
21
()
(
)
DQ
DQ
if and only if
12
()
(
)
g
Qg
Q
.
Theorem 2.
In
formal cont
ext
(,
,
)
I
,
A
, if
A
doesn’t lie at the con
s
eq
uent
of
any rule
s of
R
, then
A
is a necessary p
r
op
o
s
ition of
.
Proof.
Sinc
e
A
doesn’t lie at the con
s
e
quent of any
rule
s of
R
, it implies for
any
2
A
Q
(
2
A
denote the
po
wer se
t of
A
),
QA
doesn’t
hold,
and
there
f
ore
()
(
)
DA
D
, and thi
s
m
e
ans
A
must be
contai
ned
in
re
d
. By definition
9, we
kno
w
A
is a
necessa
ry propo
sition of
.
Corollar
y
2.1.
In
formal context
(,
,
)
I
,
A
,
A
is a necessa
ry propo
sitio
n
if
()
0
vA
and
()
1
vB
for any
BA
.
Corollar
y
2.2
.
If
A
is a usef
ul prop
ositio
n
of
, if and only if it lies at the ante
c
ed
en
t of
some rule
s
of
R
.
Theorem 3
In
formal co
ntext
(,
,
)
I
,
A
,
A
is the set of all nece
s
sary propo
si
tion
of
,
A
is a usele
ss p
r
op
ositio
n if and only if there is a su
bset
A
Q
that makes
QA
holds.
Proof.
A
is
a usel
ess
p
r
op
osition
re
d
A
red
A
Q
, that mak
e
s
QA
hold
s
.
Corollar
y
3.1.
In
formal
co
ntext
(,
,
)
I
,
A
,
A
is the
set
of all n
e
cessary
prop
ositio
n o
f
, if there exists a sub
s
et
A
Q
, and
()
1
vQ
implies
()
1
vA
, then
A
is a
usel
ess prop
osition.
Theorem 4.
In
formal co
n
t
ext
(,
,
)
I
,
Q
is a
re
ductio
n
of
, if and only if for any
2
Q
P
(
2
Q
denote the
power set of
Q
)
, there must e
x
ist a con
c
ept
who
s
e intent
is equal to
P
.
Proof.
(p
ro
of
by co
ntradi
cti
on) S
uppo
se
i
n
form
al cont
ext
(,
,
)
I
,
there do
esn’t exis
t
a con
c
e
p
t wh
ose inte
nt is equal to
P
.
Acco
rdi
ng to
the prope
rty of formal
co
ntext, we ha
ve
((
)
)
Pf
g
P
.
As
there doe
sn’t
exist a con
c
e
p
t whose inte
nt is equal to
P
, s
o
in
((
)
)
Pf
g
P
equivalent relatio
n
doesn’t hol
d,
and thu
s
((
)
)
Pf
g
P
. Moreove
r
((
)
)
Pf
g
P
P
can
be de
rived from
((
)
)
Pf
g
P
, and this
implies that t
here
mu
st b
e
a p
r
opo
sition
((
)
)
qf
g
P
P
whi
c
h
ma
ke
s
()
(
)
DQ
DQ
p
, and this
is co
ntradi
ct to the claim
Q
is a
redu
ction of
.
A redu
ction
of a propo
sit
i
on set is
co
mpos
ed of n
e
ce
ssary p
r
o
positio
ns a
n
d
useful
prop
ositio
ns.
In orde
r to find a red
u
ctio
n
of a giv
en propo
sition set, the first step
is to find all the
necessa
ry propo
sition
s,
and the next step is to find minimal num
ber of u
s
eful
prop
ositio
ns f
r
om
whi
c
h all the
other p
r
op
osit
ions
can b
e
d
edu
ced.
The followi
ng
algorithm i
s
to find a redu
ction of a prop
osition
set.
Algorithm 1.
Find a re
du
ction of a given prop
ositio
n set:
Input:
formal context
(,
,
)
I
.
Output:
re
d
(a reduc
tion of
)
Step1:
Del
e
te re
dund
ant rows an
d colu
mns
(who
se
element
s a
r
e
entirely
comp
ose
d
of
1 or 0);
Step2:
Find a
ll the nece
s
sa
ry prop
ositio
n
s
ba
sed o
n
Corolla
ry 2.1;
Step3:
Find a
ll the usele
s
s prop
ositio
ns
based on
Corollary 3.1;
Step4:
Delete
the column l
abele
d
with u
s
ele
s
s pro
p
o
s
ition
s
form the formal
con
t
ext;
Step5:
Comp
ute useful p
r
o
positio
n set;
Step6:
Cons
truc
t c
o
ncept lattic
e
of
the clarified form
al
context;
Step7:
Mining
asso
ciation rules by u
s
ing
in
tent redu
cti
on of every concept;
Step8:
Com
p
u
t
e redu
ction o
f
:
8-1: initialize
red
A
;
8-2: whil
e
B
is not empty do the followin
g
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NI
KA
Vol. 12, No. 7, July 201
4: 5567 – 55
74
5572
(1)
rand
omly sele
ct a pro
p
o
sition form
B
and move it to
re
d
;
(2) if there exist
2
re
d
Q
and a
s
soci
ation rule
i
QA
, then delete
i
A
from
B
.
8-3: retu
rn re
sult
re
d
.
The rest
of this section is
a sim
p
le example,
which i
s
presented to
vividly illustrate our
method
s on
ce more.
Exam
ple 2.
1
2345
6
{,
,
,
,
,
}
A
AA
A
A
A
,
11
A
p
,
22
3
A
pp
,
12
3
3
()
pp
p
A
,
42
A
p
,
52
3
3
2
()
()
A
pp
p
p
,
1
62
3
pp
Ap
. Formal context
(,
,
)
I
deduced
by
is sho
w
n i
n
Table 1.
Table 1. Fo
rmal Context
(,
,
)
I
1
A
2
A
3
A
4
A
5
A
6
A
1
v
(0,0,0)
*
* *
2
v
(1,0,0)
* *
* *
*
3
v
(0,1,0)
*
4
v
(0,0,1)
* *
* * *
5
v
(1,1,0)
*
*
*
6
v
(1,0,1)
*
* *
* * *
7
v
(0,1,1)
*
*
8
v
(1,1,1)
*
*
*
Step1:
Delete the 6
th
row f
o
rm the form
al context.
Step2:
Find all the necessary pro
p
o
s
itio
ns ba
se
d on
Corolla
ry 2.1:
41
4
(
)
0
,
{
2
,3
,
4
,5
,
6
}
,
(
)
0
i
vA
i
v
A
1
A
is a necessa
ry prop
ositio
n
.
25
2
(
)
0
,
{
1
,2
,
3
,4
,
6
}
,
(
)
0
i
vA
i
v
A
5
A
is a ne
ce
ssary propo
sition.
So
15
{,
}
A
A
A
.
Step3:
Find a
ll the usele
s
s prop
ositio
ns
based on
Corollary 3.1:
51
5
5
()
1
,
(
)
1
vA
vA
implies
56
()
1
vA
6
A
is an unne
ce
ssary
prop
ositio
n.
So
6
{}
C
A
.
Step4:
Delete the colum
n
labele
d
with
6
A
form the form
al context.
Step5:
Comp
ute useful p
r
o
positio
n set:
23
4
{,
,
}
BA
C
A
AA
.
Step6:
Const
r
uct
con
c
ept l
a
ttice of the clarified form
al
context (Tabl
e 2):
There are 1
2
co
nce
p
ts i
n
the co
nce
p
t lattice, i.e.
#1
1
23457
8
(
{
,,
,,
,,
}
,
{
}
)
vv
v
v
v
v
v
, #2
12
4
7
8
2
(
{
,,
,,
}
,
{
}
)
vv
v
v
v
A
,
#
3
24
7
8
2
3
({
,
,
,
}
,
{
,
}
)
vvv
v
A
A
,
#
4
345
5
({
,
,
},
{
}
)
vv
v
A
,
#5
25
8
1
({
,
,
}
,
{
}
)
vv
v
A
,
#6
12
4
2
4
({
,
,
},
{
,
}
)
vv
v
A
A
,
#7
2
4
234
({
,
}
,
{
,
,
})
vv
A
A
A
,
#8
28
1
2
3
({
,
}
,
{
,
,
})
vv
A
A
A
,
#9
21
2
3
4
(
{
},
{
,
,
,
})
vA
A
A
A
,
#10
4
2345
(
{
},
{
,
,
,
})
vA
A
A
A
,
#11
51
5
(
{
},
{
,
})
vA
A
, and
#1
2
1
2345
({}
,
{
,
,
,
,
}
)
A
AA
AA
.
Table 2. Cla
r
i
f
ied Formal
Context
1
A
2
A
3
A
4
A
5
A
1
v
(0,0,0)
* *
2
v
(1,0,0)
*
* * *
3
v
(0,1,0)
*
4
v
(0,0,1)
* * *
*
5
v
(1,1,0)
*
*
7
v
(0,1,1)
*
*
8
v
(1,1,1)
* *
*
Evaluation Warning : The document was created with Spire.PDF for Python.
TELKOM
NIKA
ISSN:
2302-4
046
Red
u
ctio
n on
Propo
sitional
Logic Set Ba
sed o
n
Co
rrel
ation Analysi
s
(Zhi
Huilai
)
5573
Step7:
Mining
associ
ation rules by u
s
ing
intent redu
cti
on:
There
a
r
e
5 con
c
e
p
ts ca
n
be used
to
derive as
so
ci
ation rule
s, while form the
other 7
con
c
e
p
ts no
asso
ciation rules
can b
e
d
e
rived.
Intent redu
ct
ion of
#3
24
7
8
2
3
({
,
,
,
}
,
{
,
}
)
vvv
v
A
A
is
3
A
and we
get associ
ation rule
13
2
:
rA
A
；
Intent red
u
cti
on of
#6
12
4
2
4
({
,
,
}
,
{
,
})
vv
v
A
A
is
4
A
a
nd we get a
s
so
ciation
rule
24
2
:
rA
A
；
Intent redu
ction of
#7
2
4
234
({
,
}
,
{
,
,
})
vv
A
A
A
is
23
and
we g
e
t a
s
soci
ation rule
32
3
4
:
rA
A
A
；
Intent redu
ction of
#8
28
1
2
3
({
,
}
,
{
,
,
})
vv
A
A
A
is
12
A
A
or
13
and
we get associ
ation rule
s
41
2
3
:
rA
A
A
and
51
3
2
:
rA
A
A
；
Intent re
du
ction of
#9
21
2
3
4
(
{
},
{
,
,
,
})
vA
A
A
A
is
14
a
n
d
we
get a
ssociatio
n rule
61
4
2
3
:
rA
A
A
A
.
So the rule set
12
3
4
5
6
, ,
, ,
,
{}
rr
r
r
r
Rr
S
.
Step8:
Comp
ute redu
ction
of
We first initial
i
ze
red
A
, and randomly sele
ct a prop
ositio
n
form
B
and move it to
re
d
. For exam
pl
e, we
sele
ct
2
A
, and
remove
it from
B
to
re
d
. Then
by u
s
ing
41
2
3
:
rA
A
A
,
we delete
3
A
from
B
; by usi
ng
32
3
4
:
rA
A
A
,
we
delete
4
A
from
B
. Then
B
is e
m
pty and
we
get the re
sult
12
5
,,
{}
red
A
AA
.
Cha
nge the
sele
ction o
r
d
e
r, we c
an
get the othe
r two re
du
ctions:
13
5
}
,
{,
A
AA
and
14
5
}
,
{,
A
AA
.
4. Conclusio
n
In this pap
er,
we p
r
e
s
ent
a new
app
ro
ach,
which is base
d
on F
C
A, for the
efficient
redu
ction
of t
w
o-val
ued
p
r
opo
sition
set.
A ba
si
s i
s
a
set
of n
o
n
-
redun
dant
pro
positio
ns fro
m
whi
c
h all p
r
o
positio
ns
can
be derive
d
, thus it c
aptures all u
s
eful i
n
formatio
n. The app
ro
ach
is
reali
z
ed
by u
s
ing
correlati
on a
nalysi
s
,
and th
e mai
n
idea
is to f
i
nd the
rel
a
tionship b
e
twe
en
prop
ositio
ns,
and discove
r
the feature
of different
kind
s of pro
positio
n. In our re
se
arch,
the
theory of fo
rmal con
c
ept
analy
s
is is
adopte
d
to
mining
asso
ciation rule
s
whi
c
h i
s
u
s
e
d
to
ascertai
n re
d
unda
nt prop
o
s
ition
s
.
Our ap
proa
ch has a twof
old advantag
e: on one
h
and, it is correlation a
nal
ysis that
make
s it diffe
rent fro
m
oth
e
r meth
od, a
s
it ca
n
expla
i
n the redu
ction proc
ess b
y
pointing o
u
t the
asso
ciation
rules whi
c
h
are u
s
ed i
n
d
e
l
e
ting no
n-
ne
ce
ssary p
r
op
osition
s
fo
rm
the p
r
op
ositi
on
set.
Wh
en ap
plying
this m
e
thod
in co
m
puter-aid
ed system,
the
u
s
ers
will have confid
en
ce whe
n
usin
g this
sy
stem ju
st be
cause they kn
ow the
run
n
i
ng me
cha
n
ics of the
syst
em. On the o
t
her
hand, it ha
s
redu
ce
d com
p
lexity, beca
u
se
of deleti
ng re
dun
dant
rows a
nd column
s form
the
context before comp
uting
a redu
ction.
But there
a
r
e
still p
r
obl
em
s left in
this
pape
r. If the
establi
s
h
ed
a
s
soci
ation
rul
e
set is
extremely large, the organization of set will
becom
e
a problem, whi
c
h
will be left for furt
her
resea
r
ch. Mo
reove
r
, ho
w t
o
ma
ke
ou
r
method
to b
e
mo
re
so
phi
sticate
d
to
a
c
commo
date
n-
valued propo
sition is a
noth
e
r impo
rt
ant probl
em for furthe
r re
sea
r
ch.
The wo
rk pre
s
ente
d
in this paper i
s
su
p
por
ted by National Scie
nce
Foundatio
n of China
(Grant No. 6
0975
033
) an
d Do
ctorial F
ound
ation of
He’n
an Polytech
nic
Unive
r
sity (G
rant
No.
B2011
-10
2
).
Referen
ces
[1]
J Do
yle. A T
r
uth Mainte
na
nce
S
y
stem.
Artificial Intelligence.
1979; 1
2
(3): 2
51-2
72.
[2]
Paol
o L
i
b
e
rato
re. Re
dun
da
nc
y
in
lo
gic I: C
N
F
prop
ositi
o
n
a
l formu
la
e.
Artificial Int
e
lligence.
20
05
;
163(
2): 203-
23
2.
[3]
Alle
n
Gins
berg
.
Know
led
ge-B
a
se R
e
d
u
ctio
n
:
A New
Ap
pr
oach
to C
hec
king k
now
le
dg
e Bas
e
s fo
r
Inconsiste
ncy and Red
u
n
d
a
n
cy.
Natio
nal
Confer
ence
o
n
Artificia
l
Intelli
ge
nce- AA
AI. Saint Pau
l
.
198
8: 585-
589.
Evaluation Warning : The document was created with Spire.PDF for Python.
ISSN: 23
02-4
046
TELKOM
NI
KA
Vol. 12, No. 7, July 201
4: 5567 – 55
74
5574
[4]
P Lib
e
rator
e
. Compi
l
a
b
il
it
y
a
nd com
pact re
prese
n
tatio
n
s
of revisi
on
of horn k
n
o
w
l
e
dg
e bas
es.
ACM
T
r
ansactio
n
s o
n
Co
mp
utatio
n
a
l Lo
gic
. 20
00; 1(1): 131-
16
1.
[5]
Dub
o
is D,
Pra
de H, et a
l
. Ch
eckin
g
t
he c
o
h
e
renc
e an
d re
dun
da
nc
y of fu
zz
y
kn
o
w
l
e
d
g
e
bases
. IEEE
Tra
n
s
a
c
ti
on
s on
Fu
z
z
y System
s
. 19
97; 5(3):
398-4
17.
[6]
J Schmolze, W
Sny
d
er.
D
e
tec
t
ing r
e
d
und
ant
prod
uction
ru
le
s
. Procee
di
ngs
of th
e F
o
urtee
n
th N
a
tio
n
a
l
Confer
ence
on
Artificial Intell
i
genc
e (AAAI’9
7). Provide
n
ce.
199
7: 417-
423.
[7]
D Maier. Minim
u
m covers
in r
e
lati
ona
l data
b
a
se mod
e
l.
Jou
r
nal of the AC
M.
1980; 27(
4): 664–
67
4.
[8]
G Ausiello, A D’Atri, et
a
l
. Minim
a
l re
pr
esentati
on
of
directe
d
h
y
p
e
r
grap
hs.
SIAM Journal
on
Co
mp
uting.
1
9
8
6
; 15(2): 41
8-4
31.
[9]
E
Hemaspaand
ra, G Wechsung.
T
he
min
i
mi
z
a
ti
on
prob
le
m for Boole
an fo
rmu
l
as.
Proce
edi
ngs of th
e
38th A
n
n
ual
S
y
mp
osi
u
m o
n
t
he F
o
un
datio
n
s
of C
o
mp
uter
Scie
nce
(F
OCS’97). M
i
ami
B
each
.19
97:
575-
584.
[10]
Maed
a M,
Oda M, et al.
Red
u
ction
meth
od
s of fu
zz
y
infe
rence ru
les w
i
th neur
al n
e
tw
ork lear
nin
g
algorithm
.
IEEE Inter
national Confer
ence on
S
y
stems, Man
,
and C
y
ber
neti
cs.
T
o
kyo. 199
9: 262-2
67.
[11]
Scaife M, R
o
g
e
rs Y. Ext
e
rna
l
cogn
itio
n: ho
w do
grap
hica
l r
epres
entati
ons
w
o
rk.
Intern
ati
ona
l Jo
urna
l
of Human C
o
mputer Studi
es.
199
6; 45: 185-
213.
[12]
Li Li-fe
ng, Z
hang D
ong-
xia
o
.
T
he Applicat
ion of
Co
ncep
t Lattice
T
heo
r
y
in the R
e
d
u
ction of th
e
Propos
ition S
e
t in T
w
o-V
a
l
ued
Propositi
o
n
a
l Log
ic.
Acta Electronica Sinica
.
2007; 3
5
(8): 1
538-
154
2.
[13]
Melvin F
i
ttin
g
. F
i
rst-order lo
gi
c and aut
om
at
ed theor
em pro
v
ing. Ne
w
Y
o
rk
: Springer. 19
9
6
.
[14]
Ganter B, W
ille
R. Formal Con
c
ept
Anal
ys
is: Mathematic
al
Found
atio
ns.
Berlin:
Spr
i
ng
er.
199
9.
[15]
Xi
e Z
h
i-p
eng,
Liu Z
o
n
g
-t
ian.
Intent reduct of concept
la
ttice node
an
d its computin
g.
Comput
e
r
Engi
neer
in
g.
2001; 27(
3): 9-11.
[16]
Z
h
i hu
il
ai, L
i
u z
ongti
an. Ev
ent
Relati
ons
hip
A
nal
ysis
Bas
ed
on F
o
rma
l C
o
n
c
ept An
al
ysis.
I
n
ternati
o
n
a
l
Confer
ence
on
Computer Sci
enc
e a
nd Soft
w
a
re Engin
eer
i
ng.
W
uhan. 2
0
08: 111
4-1
116.
[17]
Pasqu
i
er N, Bastide Y, et al.
Prunin
g
close
d
items
e
t lattic
e
s for associati
on rul
e
s.
Proceed
ings of t
h
e
14th BDA Co
nf
erenc
e. Hamm
amet. 1998: 1
7
7
-19
6
.
Evaluation Warning : The document was created with Spire.PDF for Python.