Выполнимость ярких формул
Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього. We investigate one solvable subclass of quantified formulas in pure predicate calculus and obtain a necessary and suffi...
Gespeichert in:
| Veröffentlicht in: | Український математичний журнал |
|---|---|
| Datum: | 2007 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут математики НАН України
2007
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/172501 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-172501 |
|---|---|
| record_format |
dspace |
| spelling |
Денисов, А.С. 2020-11-02T16:53:29Z 2020-11-02T16:53:29Z 2007 Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. 1027-3190 https://nasplib.isofts.kiev.ua/handle/123456789/172501 510.51 Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього. 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. ru Інститут математики НАН України Український математичний журнал Короткі повідомлення Выполнимость ярких формул Satisfiability of bright formulas Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Выполнимость ярких формул |
| spellingShingle |
Выполнимость ярких формул Денисов, А.С. Короткі повідомлення |
| title_short |
Выполнимость ярких формул |
| title_full |
Выполнимость ярких формул |
| title_fullStr |
Выполнимость ярких формул |
| title_full_unstemmed |
Выполнимость ярких формул |
| title_sort |
выполнимость ярких формул |
| author |
Денисов, А.С. |
| author_facet |
Денисов, А.С. |
| topic |
Короткі повідомлення |
| topic_facet |
Короткі повідомлення |
| publishDate |
2007 |
| language |
Russian |
| container_title |
Український математичний журнал |
| publisher |
Інститут математики НАН України |
| format |
Article |
| title_alt |
Satisfiability of bright formulas |
| description |
Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього.
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.
|
| issn |
1027-3190 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/172501 |
| citation_txt |
Выполнимость ярких формул / А.С. Денисов // Український математичний журнал. — 2007. — Т. 59, № 10. — С. 1432–1435. — Бібліогр.: 4 назв. — рос. |
| work_keys_str_mv |
AT denisovas vypolnimostʹârkihformul AT denisovas satisfiabilityofbrightformulas |
| first_indexed |
2025-11-24T11:39:54Z |
| last_indexed |
2025-11-24T11:39:54Z |
| _version_ |
1850845870971420672 |
| 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
|