D:\User\sbornik_38_pdf\18.DVI


Mathematical Problems of Computer Science 38, 42{43, 2012.

On some Systems of M inimal P r opositional Logic with

Loop Detection M echanisms

H o vh a n n e s B o lib e kya n

Department of Informatics and Applied Mathematics,
Yerevan State University, Armenia

bolibekhov@ysu.am

B a c kwa r d s p r o o f s e a r c h a n d t h e o r e m p r o vin g wit h a s t a n d a r d c u t -fr e e c a lc u lu s fo r t h e
p r o p o s it io n a l fr a g m e n t o f m in im a l lo g ic is in s u ± c ie n t b e c a u s e o f t h r e e p r o b le m s . Fir s t ly, t h e
p r o o f s e a r c h is n o t in g e n e r a l t e r m in a t in g c a u s e d b y t h e p o s s ib ilit y o f lo o p in g . S e c o n d ly, it
m ig h t g e n e r a t e p r o o fs wh ic h a r e p e r m u t a t io n s o f e a c h o t h e r a n d r e p r e s e n t t h e s a m e n a t u r a l
d e d u c t io n . Fin a lly, d u r in g t h e p r o o f s o m e c h o ic e s h o u ld b e m a d e t o d e c id e wh ic h r u le s t o
a p p ly a n d wh e r e t o u s e t h e m .

S e ve r a l p r o o f s ys t e m s o f I.Jo h a n s s o n 's m in im a l lo g ic o f p r e d ic a t e s we r e in t r o d u c e d in [1 ].
L o o p in g is t h e m a in is s u e in t h e p r o p o s it io n a l fr a g m e n t o f t h e s ys t e m GM¡ d e ve lo p e d in
[1 ]. L o o p in g m a y e a s ily b e r e m o ve d b y c h e c kin g if a s e qu e n t h a s a lr e a d y o c c u r e d in t h e
b r a n c h . Th o u g h t h is in s u ± c ie n t a s it r e qu ir e s m u c h in fo r m a t io n t o b e s t o r e d . S o m e lo o p in g
m e c h a n is m s h a ve b e e n c o n s id e r e d e a r lie r in [2 ,3 ].

On e wa y t o d e t e c t lo o p s is a d d in g h is t o r y t o e a c h s e qu e n t . Th e h is t o r y is a s e t o f s e qu e n t s
t h a t h a ve o c c u r e d s o fa r in t h e b r a n c h o f a p r o o f t r e e . A ft e r e a c h b a c kwa r d s in fe r e n c e t h e
n e w s e qu e n t is ve r ī e d if it is in t h is s e t . If it is we h a ve lo o p in g a n d b a c kt r a c k. Ot h e r wis e
t h e n e w h is t o r y is t h e e xt e n s io n o f t h e o ld h is t o r y b y t h e o ld s e qu e n t . Th is m e t h o d is
u n s u ± c ie n t a s it r e qu ir e s m u c h in fo r m a t io n r e p r e s e n t e d a s lis t o f s e qu e n t s t o b e s t o r e d a n d
o n e a c h s t e p t h is lis t s s h o u ld b e c h e c ke d . To im p r o ve t h e e ± c ie n c y s o m e m e c h a n is m s a r e
r e qu ir e d t o c u t d o wn t h e a m o u n t o f s t o r a g e a n d c h e c ks n e e d e d t o p r e ve n t lo o p in g . In fa c t
t o r e d u c e t h e h is t o r y we n e e d o n ly s t o r e g o a l fo r m u la e in o r d e r t o c h e c k lo o p s . U s in g t h e
r u le s o f GM¡ t h e c o n t e xt c a n n o t d e c r e a s e : o n c e a fo r m u la is in a c o n t e xt it will b e in t h e
c o n t e xt o f a ll t h e s e qu e n t s a b o ve it in t h e p r o o f t r e e . S o t h e s e qu e n t s t o b e t h e s a m e t h e y
n e e d t o h a ve t h e s a m e c o n t e xt . Th e r e fo r e we m a y e m p t y t h e h is t o r y e ve r y t im e t h e c o n t e xt
is e xt e n d e d . On ly g o a l fo r m u la e a r e n e e d e d t o b e s t o r e d in t h e h is t o r y. If t h e r e is a s e qu e n t
wh o s e g o a l is a lr e a d y in t h e h is t o r y, t h e n we h a ve t h e s a m e g o a l a n d t h e s a m e c o n t e xt a s
a n o t h e r s e qu e n t , s o lo o p in g o c c u r e d .

W e in t r o d u c e t wo s ys t e m s fo r p r o p o s it io n a l fr a g m e n t o f m in im a l lo g ic wh ic h a r e s lig h t ly
d i®e r e n t . B o t h s ys t e m s a r e b a s e d o n t h e id e a o f a d d in g c o n t e xt t o t h e s e qu e n t s . In o n e
s ys t e m , SwM in, t h e h is t o r y is ke p t s m a lle r , b u t ScM in d e t e c t s lo o p s m o r e qu ic kly. Th e
h e a r t o f t h e d i®e r e n c e b e t we e n t h e t wo s ys t e m s is t h a t in t h e SwMin lo o p c h e c kin g is d o n e
wh e n a fo r m u la le a ve s t h e g o a l, wh e r e a s in t h e ScMin it is d o n e wh e n it b e c o m e s t h e g o a l.

4 2



H. Bolibekyan 4 3

T heor em

1 . Th e s ys t e m s GM¡ a n d SwMin a r e e qu iva le n t .
2 . Th e s ys t e m s GM¡ a n d ScM in a r e e qu iva le n t .

Acknowledgment. Th is wo r k is s u p p o r t e d b y Gr a n t 1 1 -1 b 0 2 3 o f S S C o f t h e Go ve r m e n t
o f A r m e n ia .

R e fe r e n c e s

[1 ] B o lib e kya n H .R ., Ch u b a r ya n A .A ., On s o m e p r o o f s ys t e m s fo r I.Jo h a n s s o n 's m in im a l
lo g ic o f p r e d ic a t e s , P r o c e e d in g s o f t h e L o g ic Co llo qu iu m 2 0 0 3 , p . 5 6 .

[2 ] Ga b b a y D ., A lg o r it h m ic p r o o f wit h d im in is h in g r e s o u r c e s , P a r t 1 , S p r in g e r L e c t u r e N o t e s
in Co m p u t e r S c ie n c e , 5 3 3 , p p . 1 5 6 -1 7 3 , 1 9 9 1

[3 ] B o lib e kya n H ., Mu r a d ya n T., On s o m e lo o p d e t e c t io n s t r a t e g ie s fo r m in im a l p r o p o s it io n a l
lo g ic , P r o c e e d in g s o f t h e L o g ic Co llo qu iu m 2 0 1 1 , p . 4 5 -4 6 .