Выполнимость ярких формул
Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього....
Збережено в:
| Дата: | 2007 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут математики НАН України
2007
|
| Назва видання: | Український математичний журнал |
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/172501 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-172501 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-1725012020-11-03T01:27:03Z Выполнимость ярких формул Денисов, А.С. Короткі повідомлення Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього. We investigate one solvable subclass of quantified formulas in pure predicate calculus and obtain a necessary and sufficient condition for the satisfiability of formulas from this subclass. 2007 Article Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. 1027-3190 http://dspace.nbuv.gov.ua/handle/123456789/172501 510.51 ru Український математичний журнал Інститут математики НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Короткі повідомлення Короткі повідомлення |
| spellingShingle |
Короткі повідомлення Короткі повідомлення Денисов, А.С. Выполнимость ярких формул Український математичний журнал |
| description |
Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього. |
| format |
Article |
| author |
Денисов, А.С. |
| author_facet |
Денисов, А.С. |
| author_sort |
Денисов, А.С. |
| title |
Выполнимость ярких формул |
| title_short |
Выполнимость ярких формул |
| title_full |
Выполнимость ярких формул |
| title_fullStr |
Выполнимость ярких формул |
| title_full_unstemmed |
Выполнимость ярких формул |
| title_sort |
выполнимость ярких формул |
| publisher |
Інститут математики НАН України |
| publishDate |
2007 |
| topic_facet |
Короткі повідомлення |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/172501 |
| citation_txt |
Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. |
| series |
Український математичний журнал |
| work_keys_str_mv |
AT denisovas vypolnimostʹârkihformul |
| first_indexed |
2025-07-15T08:48:32Z |
| last_indexed |
2025-07-15T08:48:32Z |
| _version_ |
1837702121418391552 |
| fulltext |
K�O�R�O�T�K�I���P�O�V�I�D�O�M�L�E�N�N�Q
UDK 510.51
A. S. Denysov (NYY matematyky pry Qkut. un-te, Rossyq)
VÁPOLNYMOST| QRKYX FORMUL
We investigate one of solvable subclasses of quantor formulas in the pure predicate calculus. We obtain
a necessary and sufficient condition for the realizability of formulas from this subclass.
DoslidΩu[t\sq odyn iz rozv’qznyx pidklasiv kvantornyx formul u çystomu çyslenni predykativ.
Otrymano neobxidnu ta dostatng umovu zdijsnennosti dlq formul, wo vxodqt\ do n\oho.
Problem¥ dokazuemosty y v¥polnymosty kvantorn¥x formul çystoho ysçysle-
nyq predykatov pervoho porqdka voznykly odnovremenno s poqvlenyem dannoho
lohyçeskoho ysçyslenyq. Buduçy dvojstvenn¥my, ony predstavlqgt tradycy-
onn¥j ynteres y uΩe pozvolyly poluçyt\ raznoobrazn¥e y soderΩatel\n¥e re-
zul\tat¥ [1]. Pry πtom problema v¥polnymosty okazalas\ yzuçennoj v men\-
ßej stepeny. V nastoqwej rabote predprynqta pop¥tka strohoho yzloΩenyq
razreßagwej procedur¥ dlq problem¥ v¥polnymosty kvantorn¥x formul,
matryc¥ kotor¥x soderΩat pomymo lohyçeskoj svqzky otrycanyq kak konægnk-
cyg, tak y dyzægnkcyg, na prymere qrkyx formul.
Lgbaq πlementarnaq formula çystoho ysçyslenyq predykatov ymeet vyd
P ( xi0
, … , xip
–
1
) .
Opredelenye 1. Formula ψ naz¥vaetsq sostavnoj, esly
ψ = ∀x0 … ∀xm – 1 ∃ xm … ∃ xn – 1 Φ ( x0 , … , xm – 1 , xm , … , xn – 1 ),
Φ = Φ0 ∨ Φ1
,
Φ0 = P ( xi0
, … , xip
–
1
) & �P ( xj0
, … , xjp
–
1
),
Φ1 = Q ( xip
, … , xi a
–
1
) & �Q ( xjp
, … , xj a
–
1
).
Suwestvennug rol\ pry yzuçenyy sostavn¥x formul yhraet otnoßenye tak
naz¥vaemoj ladejnoj svqznosty [2]. Ymenno, dlq çysel 0 ≤ k, l ≤ a – 1 sçytaet-
sq, çto k � l tohda y tol\ko tohda, kohda lybo
suwestvugt 0 ≤ k0 , k1 , … , kz ≤ p – 1 takye, çto k0 = k, iky
= iky
+
1
yly jk
y
= jk
y
+
1
dlq vsex 0 ≤ y ≤ z – 1, kz = l,
lybo
suwestvugt p ≤ l0 , l1 , … , lz ≤ a – 1 takye, çto l0 = k, il y = il
y
+
1
© A. S. DENYSOV, 2007
1432 ISSN 1027-3190. Ukr. mat. Ωurn., 2007, t. 59, # 10
VÁPOLNYMOST| QRKYX FORMUL 1433
yly jly
= jly
+
1
dlq vsex 0 ≤ y ≤ z – 1, lz = l.
Yssledovanye klassa sostavn¥x formul, u kotor¥x Φ0
razbyvaetsq na dva
klassa ladejnoj svqznosty v tom sm¥sle, çto
{ 0, 1, … , p – 1 } = { 0, 1, … , b – 1 } ∪ { b, b + 1, … , p – 1 },
0 ≤ k, l ≤ b – 1 vleçet k � l,
b ≤ k, l ≤ p – 1 vleçet k � l,
0 ≤ k ≤ b – 1, b ≤ l ≤ p – 1 vleçet k � l
pry nekotorom 0 < b < p, naçynaetsq so sledugweho çastnoho sluçaq.
Opredelenye 2. Sostavnaq formula opysannoho vyda naz¥vaetsq qrkoj,
esly
0 ≤ i0 , … , ib – 1 , j0 , … , jb – 1 ≤ m – 1,
m ≤ ib = … = ip – 1 , jb = … = jp – 1 ≤ n – 1,
0 ≤ ip , … , ia – 1 ≤ m – 1,
formula
ψ1 = ∀x0 … ∀xm – 1 ∃ xm … ∃ xn – 1 Φ1
( x0 , … , xm – 1 , xm , … , xn – 1 )
nev¥polnyma y uslovye m ≤ jl ≤ n – 1 vleçet
il ∉ { i0 , … , ib – 1 , j0 , … , jb – 1 }.
Teorema. Dlq toho çtob¥ qrkaq formula b¥la v¥polnymoj, neobxodymo y
dostatoçno ystynnosty neravenstva ib ≠ jb .
Dokazatel\stvo. Pust\ ψ — proyzvol\naq qrkaq formula. Rassmotrym
standartnug posledovatel\nost\ Φ0 , Φ1 , Φ2 , … , Φq , … beskvantorn¥x for-
mul, πkvyvalentnug ψ [3]. KaΩdug formulu Φq predstavym v vyde
Φq = Φq ( ccq
( 0 ) , … , ccq
( n – 1 ) )
s pomow\g funkcyy cq : { 0, … , n – 1 } → N. S druhoj storon¥, Φ q = Φq
0 ∨ Φq
1
.
Vvedem takΩe funkcyy cq
0 , cq
1
: { 0, … , a – 1 } → N, poloΩyv
c kq
0( ) = cq ( ik ),
c kq
1( ) = cq ( jk )
dlq vsex 0 ≤ k ≤ a – 1.
Fakt razreßymosty problem¥ v¥polnymosty formul, v beskvantornoj ças-
ty kotor¥x pomymo symvola � vstreçaetsq lyß\ symvol &, yzvesten so vre-
men Hyl\berta. V¥qvlenye otlyçyj, voznykagwyx v posledovatel\nosty Φ0 ,
Φ1 , Φ2 , … posle dobavlenyq symvola ∨, pryvelo k sledugwemu estestvennomu
kryteryg dlq sostavn¥x formul [4].
PredloΩenye. Sostavnaq formula ψ v¥polnyma tohda y tol\ko tohda,
kohda ymeetsq h : N → { 0, 1 } takaq, çto ne suwestvuet q, s ∈ N takyx, çto
h ( q ) = 0, h ( s ) = 0, y verna systema ravenstv
c kq
0( ) = c ks
1( ) , 0 ≤ k ≤ p – 1,
lybo h ( q ) = 1, h ( s ) = 1 y pravyl\na systema ravenstv
ISSN 1027-3190. Ukr. mat. Ωurn., 2007, t. 59, # 10
1434 A. S. DENYSOV
c kq
0( ) = c ks
1( ) , p ≤ k ≤ a – 1.
Funkcyq h, udovletvorqgwaq uslovyg πtoho predloΩenyq, naz¥vaetsq v¥-
byragwej.
Dostatoçnost\. Pust\ ib ≠ jb . V kaçestve h rassmotrym funkcyg h ≡ 0.
Tohda dlq lgb¥x q, s ∈ N po opredelenyg posledovatel\nosty Φ0 , Φ1 , Φ2 , …
… , Φq , …
c b c i c j c bq q b s b s
0 1( ) = ( ) ≠ ( ) = ( )
v sylu uslovyq m ≤ ib , jb ≤ n – 1, tak çto systema
c kq
0( ) = c ks
1( ) , 0 ≤ k ≤ p – 1,
ne moΩet b¥t\ pravyl\noj. Poskol\ku sluçaj h ( q ) = 1, h ( s ) = 1 nevozmoΩen,
po predloΩenyg ψ v¥polnyma.
Neobxodymost\. PredpoloΩym, çto ψ v¥polnyma y h — v¥byragwaq
funkcyq dlq ψ. Pust\, naoborot, ib = jb . Rassmotrym formulu
Φ0 = Φ ( c0 , … , c0 , c1 , … , cn – m ) .
Dopustym, çto h ( 0 ) = 0. Esly tohda 0 ≤ k ≤ b – 1, to po opredelenyg qrkoj
formul¥ 0 ≤ ik , jk ≤ m – 1, otkuda
c k0
0( ) = c0 ( ik ) = 0,
c k0
1( ) = c0 ( jk ) = 0
y c k0
0( ) = c k0
1( ). Esly Ωe b ≤ k ≤ a – 1, to po opredelenyg ik = jk = ib , tak çto
c k c i c j c kk k0
0
0 0 0
1( ) = ( ) = ( ) = ( ).
PoloΩyv q = 0, s = 0 v uslovyy na h, poluçym protyvoreçye.
Pust\ h ( 0 ) = 1. Opredelym nekotoroe çyslo q ∈ N sootnoßenyqmy
cq ( i ) =
c j p l a i il l0 1
0
( ) ≤ ≤ −
,
—
esly suwestvuet takoe, çto = ,
v protyvnom sluçae
dlq vsex 0 ≤ i ≤ m – 1. V sylu nev¥polnymosty ψ1 dannoe opredelenye kor-
rektno.
Zafyksyruem proyzvol\noe p ≤ l ≤ a – 1. Tohda dlq i = il v¥polneno pervoe
uslovye opredelenyq cq ( i ), otkuda
c l c i c i c j c lq q l q l
0
0 0
1( ) = ( ) = ( ) = ( ) = ( ).
Takym obrazom, systema
c lq
0( ) = c l0
1( ), p ≤ l ≤ a – 1,
pravyl\na. Tak kak h ( 0 ) = 1, to h ( q ) = 0.
Zafyksyruem teper\ 0 ≤ k ≤ p – 1. Esly 0 ≤ k ≤ b – 1, to 0 ≤ ik , jk ≤ m – 1.
V sylu posledneho punkta v opredelenyy qrkoj formul¥ çysla i = ik y i = jk
ne mohut udovletvorqt\ pervomu uslovyg v opredelenyy cq ( i ). Znaçyt,
ISSN 1027-3190. Ukr. mat. Ωurn., 2007, t. 59, # 10
VÁPOLNYMOST| QRKYX FORMUL 1435
c kq
0( ) = cq ( ik ) = 0,
c kq
1( ) = cq ( jk ) = 0
y
c kq
0( ) = c kq
1( ).
Esly Ωe b ≤ k ≤ p – 1, to ik = jk = ib , otkuda
c k c i c j c kq q k q k q
0 1( ) = ( ) = ( ) = ( ).
V rezul\tate spravedlyv¥ vse ravenstva system¥
c kq
0( ) = c kq
1( ), 0 ≤ k ≤ p – 1.
Poluçyly protyvoreçye s uslovyqmy na h. Sledovatel\no, ψ nev¥polnyma.
Teorema dokazana.
1. Börger E., Gradel E., Gurevich Yu. The classical decision problem. – Berlin etc.: Springer, 1997.
2. Denisov A. S. The satisfability in the class of composite formulas // Abstrs Logic Colloquim’95. –
Haifa (Israel), 1995. – P. 64.
3. Mal\cev A. Y. Yssledovanyq v oblasty matematyçeskoj lohyky // Yzbr. tr. T. 2. Matematy-
çeskaq lohyka y obwaq teoryq alhebrayçeskyx system. – M.: Nauka, 1976. – S. 5 – 16.
4. Denysov A. S. V¥polnymost\ al\ternatyvn¥x formul // Mat. zametky Qkut. un-ta. – 1996.
– V¥p. 1. – S. 38 – 41.
Poluçeno 05.07.2005,
posle dorabotky — 31.08.2006
ISSN 1027-3190. Ukr. mat. Ωurn., 2007, t. 59, # 10
|