Satisfiability of bright formulas
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.
Gespeichert in:
| Datum: | 2007 |
|---|---|
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Russisch Englisch |
| Veröffentlicht: |
Institute of Mathematics, NAS of Ukraine
2007
|
| Online Zugang: | https://umj.imath.kiev.ua/index.php/umj/article/view/3401 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Ukrains’kyi Matematychnyi Zhurnal |
| Завантажити файл: |  |
Institution
Ukrains’kyi Matematychnyi Zhurnal| _version_ | 1860509485410287616 |
|---|---|
| author | Denisov, A. S. Денисов, А. С. Денисов, А. С. |
| author_facet | Denisov, A. S. Денисов, А. С. Денисов, А. С. |
| author_sort | Denisov, A. S. |
| baseUrl_str | https://umj.imath.kiev.ua/index.php/umj/oai |
| collection | OJS |
| datestamp_date | 2020-03-18T19:53:10Z |
| 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. |
| first_indexed | 2026-03-24T02:41:51Z |
| format | Article |
| 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
|
| id | umjimathkievua-article-3401 |
| institution | Ukrains’kyi Matematychnyi Zhurnal |
| keywords_txt_mv | keywords |
| language | rus English |
| last_indexed | 2026-03-24T02:41:51Z |
| publishDate | 2007 |
| publisher | Institute of Mathematics, NAS of Ukraine |
| record_format | ojs |
| resource_txt_mv | umjimathkievua/80/34843afdd8bb0b8b166b14bb1dd95b80.pdf |
| spelling | umjimathkievua-article-34012020-03-18T19:53:10Z Satisfiability of bright formulas Выполнимость ярких формул Denisov, A. S. Денисов, А. С. Денисов, А. С. 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. Досліджується один із розв'язних підкласів кванторних формул у чистому численні предикатів. Отримано необхідну та достатню умову здійсненності для формул, що входять до нього. Institute of Mathematics, NAS of Ukraine 2007-10-25 Article Article application/pdf https://umj.imath.kiev.ua/index.php/umj/article/view/3401 Ukrains’kyi Matematychnyi Zhurnal; Vol. 59 No. 10 (2007); 1432–1435 Український математичний журнал; Том 59 № 10 (2007); 1432–1435 1027-3190 rus en https://umj.imath.kiev.ua/index.php/umj/article/view/3401/3545 https://umj.imath.kiev.ua/index.php/umj/article/view/3401/3546 Copyright (c) 2007 Denisov A. S. |
| spellingShingle | Denisov, A. S. Денисов, А. С. Денисов, А. С. Satisfiability of bright formulas |
| title | Satisfiability of bright formulas |
| title_alt | Выполнимость ярких формул |
| title_full | Satisfiability of bright formulas |
| title_fullStr | Satisfiability of bright formulas |
| title_full_unstemmed | Satisfiability of bright formulas |
| title_short | Satisfiability of bright formulas |
| title_sort | satisfiability of bright formulas |
| url | https://umj.imath.kiev.ua/index.php/umj/article/view/3401 |
| work_keys_str_mv | AT denisovas satisfiabilityofbrightformulas AT denisovas satisfiabilityofbrightformulas AT denisovas satisfiabilityofbrightformulas AT denisovas vypolnimostʹârkihformul AT denisovas vypolnimostʹârkihformul AT denisovas vypolnimostʹârkihformul |