Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства
The derivable rules of axiomatic extensions of sequent calculi with structural rules for the
 prepositional finitely valued logics with an equality determinant are analyzed with the use of
 methods of logic programming.
Saved in:
| Date: | 2008 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Видавничий дім "Академперіодика" НАН України
2008
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/4138 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860101030678626304 |
|---|---|
| author | Пынько, А.П. |
| author_facet | Пынько, А.П. |
| citation_txt | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. |
| collection | DSpace DC |
| description | The derivable rules of axiomatic extensions of sequent calculi with structural rules for the
prepositional finitely valued logics with an equality determinant are analyzed with the use of
methods of logic programming.
|
| first_indexed | 2025-12-07T17:28:53Z |
| format | Article |
| fulltext |
оповiдi
НАЦIОНАЛЬНОЇ
АКАДЕМIЇ НАУК
УКРАЇНИ
4 • 2008
IНФОРМАТИКА ТА КIБЕРНЕТИКА
УДК 510.6
© 2008
А.П. Пынько
Производные правила секвенциальных исчислений
для конечнозначных логик с определителем равенства
(Представлено членом-корреспондентом НАН Украины А.А. Летичевским)
The derivable rules of axiomatic extensions of sequent calculi with structural rules for the
prepositional finitely valued logics with an equality determinant are analyzed with the use of
methods of logic programming.
Используя методы логического программирования, мы предлагаем процедуры поиска выво-
да производных правил секвенциальных исчислений работы [1] со структурными прави-
лами.
Будем следовать терминологии, обозначениям и установкам, принятым в работе [1].
Зафиксируем F ⊆ G ⊆ ℑ(FmL′(W )) и H ⊆ Seq
(k,l)
G .
Определение 1. C(F,G,H) — секвенциальное L-исчисление ранга (k, l), состоящее из
аксиом и правил исчисления C и следующих структурных правил:
для всех Γ ⊢ ∆ ∈ Seq
(k,l)
G и ϕ ∈ F
(сечение)
Γ, ϕ ⊢ ∆ Γ ⊢ ∆, ϕ
Γ ⊢ ∆
;
для всех Γ ⊢ ∆ ∈ H и ϕ ∈ G
(утончение слева)
Γ ⊢ ∆
ϕ,Γ ⊢ ∆
,
(утончение справа)
Γ ⊢ ∆
Γ ⊢ ϕ,∆
.
Определение 2. Понятие нормального C(F,G,H)-вывода Γ ⊢ ∆ ∈ Seq
(k,l)
G из T ∈
∈ (Seq
(k,l)
F
⋂
H)∗ как основного терма сигнатуры L
⋃
Var
⋃
{sq}
⋃
ω со списковыми и до-
полнительными символами g, pr, ax, cut, lw, rw, lr и rr арностей 3, 1, 4, 0, 0, 0, 4 и 3,
соответственно, определяется рекурсивно следующим образом:
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2008, №4 51
всякий C-вывод Γ ⊢ ∆ является нормальным C(F,G,H)-выводом Γ ⊢ ∆ из T ;
всякий терм вида g(sq(Γ,∆), pr(s), []), где s ∈ |T |, является нормальным C(F,G,H)-выво-
дом Γ ⊢ ∆ из T , если Γ ⊢ ∆ = T s;
для всех ϕ ∈ F всякий терм вида g(sq(Γ,∆), cut, [f, h]), где f и h — нормальные
C(F,G,H)-выводы Γ, ϕ ⊢ ∆ и Γ ⊢ ∆, ϕ, соответственно, из T , является нормальным
C(F,G,H)-выводом Γ ⊢ ∆ из T ;
для всех ϕ ∈ G всякие термы вида g(sq((ϕ,Γ),∆), lw, [f ]) и g(sq(Γ, (ϕ,∆)), rw, [f ]), где
f — нормальный C(F,G,H)-вывод Γ ⊢ ∆ из T , являются нормальными C(F,G,H)-выводами
ϕ, Γ ⊢ ∆ и Γ ⊢ ϕ, ∆, соответственно, из T , если Γ ⊢ ∆ ∈ H.
Определение 3. Пролог-программа Q состоит из следующих предложений1 :
der([], sq(X, Y), G) : −seq(X, [], Y, [], [], G). (1)
der([sq(W, Z)|T], sq(X, Y), G) : −ded(T, W, Z, [], [], X, Y, G). (2)
ded(T, [], [], A, B, [], [], g(sq(L, R), pr(N), [])) : − (3)
length(T, N), reverse(A, L), reverse(B, R).
ded(T, [], [], A, B, [F|X], Y, g(sq([F|L], R), wl, [G])) : − (4)
reverse(A, C), reverse(B, D),
append(X, C, L), append(Y, D, R), ded(T, [], [], A, B, X, Y, G).
ded(T, [], [], A, B, [], [F|Y], g(sq(L, [F|R]), wr, [G])) : −
reverse(A, L), reverse(B, D),
append(Y, D, R), ded(T, [], [], A, B, [], Y, G).
ded(T, [F|I], J, A, B, X, Y, g(sq(L, R), cut, [G, H])) : − (5)
reverse(A, C), reverse(B, D),
append(X, C, L), append(Y, D, R), append(R, [F], E),
der(T, sq(L, E), H), ded(T, I, J, [F|A], B, X, Y, G).
ded(T, [], [F|J], A, B, X, Y, g(sq(L, R), cut, [G, H])) : −
reverse(A, C), reverse(B, D),
append(X, C, L), append(Y, D, R), append(L, [F], E),
der(T, sq(E, R), G), ded(T, [], J, A, [F|B], X, Y, H).
Положим R := P
⋃
Q при |L′| < ω.
Теорема 1. Пусть T ⊆ ωSeq
(k,l)
F
⋂
H и Γ ⊢ ∆ ∈ Seq
(k,l)
G . Предположим, что ~ℑ —
последовательность, не убывающая относительно �2, а H — верхний конус 〈Seq
(k,l)
G ,⊑〉.
Тогда:
1Определения встроенных в систему SWI-Prolog (см. http://swi.psy.uva.nl/projects/SWI-Prolog/) преди-
катов length/2, reverse/2 и append/3 опущены.
2См. сноску 4 работы [1].
52 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2008, №4
1) при |L′| < ω запрос der(~T, sq(Γ,∆), G) получает в программе R положительный
ответ с решением G = нормальный C(F,G,H)-вывод Γ ⊢ ∆ из ~T , если Γ ⊢ ∆ ∈ Cn
(k,l)
M
(T ),
и отрицательный ответ — в противном случае;
2) следующие утверждения эквивалентны:
а) Γ ⊢ ∆ имеет нормальный C(F,G,H)-вывод из ~T ;
б) T → Γ ⊢ ∆ — производное правило исчисления C(F,G,H);
в) Γ ⊢ ∆ ∈ Cn
(k,l)
M
(T ).
Доказательство. Докажем утверждение 1 индукцией по мощности |T | запроса вида,
указанного в его формулировке, называя его начальным, а Γ ⊢ ∆ — его характеристической
секвенцией.
Пусть T = ∅. Тогда к рассматриваемому начальному запросу применяется только пра-
вило (1), причем он получает в R отрицательный (положительный) ответ (с решением G = t,
где t — произвольный терм), если запрос seq(Γ, [],∆, [], [], G) получает в P отрицательный
(положительный) ответ (с тем же решением G = t). Тем самым теорема 1 работы [1] завер-
шает анализ случая T = ∅.
Предположим, что T 6= ∅. Тогда ~T = (Θ ⊢ Ξ; ~S), где Θ ⊢ Ξ ∈ T и S := T \{Θ ⊢ Ξ}. Тогда,
к рассматриваемому начальному запросу применяется только правило 2, причем он полу-
чает в R отрицательный (положительный) ответ (с решением G = t, где t — произвольный
терм), если запрос ded(~S,Θ,Ξ, [], [],Γ,∆, G) получает в R отрицательный (положительный)
ответ (с тем же решением G = t). Запрос вида ded(~S,Σ,Ω,Λ,Π,Γ,∆, G), где Θ = (Λ,Σ),
Ξ = (Π,Ω) и Γ ⊢ ∆ ∈ Seq
(k,l)
G , назовем регулярным, причем Γ, Λ ⊢ ∆, Π ∈ Seq
(k,l)
G будем
называть его характеристической секвенцией, а |Σ| + |Ω| + |Γ| + |∆| — его сложностью,
индукцией по которой докажем, что он получает в R положительный ответ с решением
G = нормальный C(F,G,H)-вывод его характеристической секвенции из ~T , если она при-
надлежит Cn
(k,l)
M
(T ), и отрицательный ответ — в противном случае. При этом регулярный
запрос вида ded(~S, [], [],Λ,Π,Γ,∆, G) будем называть простым. Заметим, что характеристи-
ческая секвенция всякого простого запроса ⊒ Θ ⊢ Ξ и поэтому принадлежит Cn
(k,l)
M
(T )
⋂
H.
Пусть |Σ| + |Ω| = 0, т. е., рассматриваемый регулярный запрос является простым.
Если |Γ|+ |∆| = 0, то характеристическая секвенция рассматриваемого простого запро-
са совпадает с Θ ⊢ Ξ. Тогда к рассматриваемому простому запросу применяется только
правило 3. При этом он получает в R положительный ответ с решением G = нормальный
C(F,G,H)-вывод его характеристической секвенции из ~T , что завершает анализ случая
|Γ| + |∆| = 0.
Предположим, что |Γ| + |∆| > 0. Допустим, что |Γ| > 0, т. е., Γ = (ϕ,Υ) для некоторой
ϕ ∈ G. (Случай, когда |Γ| = 0 и, тем самым, |∆| > 0, рассматривается аналогично.) Тогда
к рассматриваемому простому запросу применяется только правило 4. При этом он полу-
чает в R положительный ответ с решением G = нормальный C(F,G,H)-вывод его харак-
теристической секвенции из ~T , если производный простой запрос ded(~S, [], [],Λ,Π,Υ,∆, G)
сложности |Σ| + |Ω| + |Υ| + |∆| < |Σ| + |Ω| + |Γ| + |∆| получает в R положительный ответ
с решением G = нормальный C(F,G,H)-вывод его характеристической секвенции из ~T .
Таким образом, индукция по сложности регулярных запросов завершает анализ случая
|Γ| + |∆| > 0 и, тем самым, случая |Σ| + |Ω| = 0.
Предположим, что |Σ| + |Ω| > 0. Допустим, что |Σ| > 0, т. е., Σ = (ϕ,Υ) для некото-
рой ϕ ∈ F . (Случай, когда |Σ| = 0 и, тем самым, |Ω| > 0, рассматривается аналогично.)
Тогда к рассматриваемому регулярному запросу применяется только правило 5. При этом
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2008, №4 53
он получает в R отрицательный (положительный) ответ (с решением G = нормальный
C(F,G,H)-вывод его характеристической секвенции из ~T ), если производный регулярный
запрос ded(~S,Υ,Ω, (ϕ,Λ),Π,Γ,∆, G) сложности |Υ| + |Ω| + |Γ| + |∆| < |Σ| + |Ω| + |Γ| +
+ |∆| получает в R отрицательный (положительный) ответ (с решением G = нормальный
C(F,G,H)-вывод его характеристической секвенции из ~T ) или (и) производный начальный
запрос der(~S, sq((Γ,Λ), (∆,Π, ϕ)), G) мощности |S| < |T | получает отрицательный (поло-
жительный) ответ (с решением G = нормальный C(F,G,H)-вывод его характеристической
секвенции из ~S). Поскольку Θ ⊢ Ξ, ϕ ∈ Cn
(k,l)
M
(∅) и характеристическая секвенция рас-
сматриваемого регулярного запроса ⊑ характеристической секвенции указанного производ-
ного, характеристическая секвенция рассматриваемого регулярного запроса принадлежит
Cn
(k,l)
M
(T ) тогда и только тогда, когда характеристическая секвенция указанного произ-
водного регулярного принадлежит Cn
(k,l)
M
(T ), а начального — Cn
(k,l)
M
(S). Таким образом,
индукция по мощности начальных запросов и сложности регулярных завершает анализ
случая |Σ|+ |Ω| > 0 и поэтому случая T 6= ∅ и, тем самым, доказательство утверждения 1.
Наконец, докажем утверждение 2. Следствие 2а ⇒ 2b тривиально, 2b ⇒ 2с вытекает из
равенств (1) и (2) работы [2], а 2с ⇒ 2а — из утверждения 1 и конечности множества всех
связок, входящих в конечное множество L-секвенций.
Замечание 1. Теорема 1 содержит теорему 1 работы [1] в качестве частного случая
при F = H = T = ∅ и G = ℑ(FmL′(W )). При F = G = ℑ(FmL′(W )) и H = Seq
(k,l)
G
утверждение 2 теоремы 1 дает теорему сильной полноты (аналог следствия 2 работы [2]),
а при F =
⋂
{E ⊆ FmL | T ⊆ Seq
(k,l)
E }, G = ℑ(FmL′(W )) и H = Seq
(k,l)
G — теорему о сильном
устранении сечения.
1. Пынько А.П. Процедуры вывода в секвенциальных исчислениях для конечнозначных логик с опре-
делителем равенства // Доп. НАН України. – 2007. – № 3. – С. 45–51.
2. Пынько А.П. Секвенциальные исчисления для конечнозначных логик с определителем равенства //
Там само. – 2003. – № 8. – С. 69–75.
Поступило в редакцию 14.11.2007Институт кибернетики им. В.М. Глушкова
НАН Украины, Киев
54 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2008, №4
|
| id | nasplib_isofts_kiev_ua-123456789-4138 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1025-6415 |
| language | Russian |
| last_indexed | 2025-12-07T17:28:53Z |
| publishDate | 2008 |
| publisher | Видавничий дім "Академперіодика" НАН України |
| record_format | dspace |
| spelling | Пынько, А.П. 2009-07-16T09:08:10Z 2009-07-16T09:08:10Z 2008 Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. 1025-6415 https://nasplib.isofts.kiev.ua/handle/123456789/4138 510.6 The derivable rules of axiomatic extensions of sequent calculi with structural rules for the
 prepositional finitely valued logics with an equality determinant are analyzed with the use of
 methods of logic programming. ru Видавничий дім "Академперіодика" НАН України Інформатика та кібернетика Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства Article published earlier |
| spellingShingle | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства Пынько, А.П. Інформатика та кібернетика |
| title | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_full | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_fullStr | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_full_unstemmed | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_short | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_sort | производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| topic | Інформатика та кібернетика |
| topic_facet | Інформатика та кібернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/4138 |
| work_keys_str_mv | AT pynʹkoap proizvodnyepravilasekvencialʹnyhisčisleniidlâkonečnoznačnyhlogiksopredelitelemravenstva |