Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства
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.
Збережено в:
| Дата: | 2008 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Видавничий дім "Академперіодика" НАН України
2008
|
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/4138 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-4138 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-41382009-12-11T14:35:16Z Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства Пынько, А.П. Інформатика та кібернетика 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. 2008 Article Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. 1025-6415 http://dspace.nbuv.gov.ua/handle/123456789/4138 510.6 ru Видавничий дім "Академперіодика" НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Інформатика та кібернетика Інформатика та кібернетика |
| spellingShingle |
Інформатика та кібернетика Інформатика та кібернетика Пынько, А.П. Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| 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. |
| format |
Article |
| author |
Пынько, А.П. |
| author_facet |
Пынько, А.П. |
| author_sort |
Пынько, А.П. |
| title |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_short |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_full |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_fullStr |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_full_unstemmed |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_sort |
производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства |
| publisher |
Видавничий дім "Академперіодика" НАН України |
| publishDate |
2008 |
| topic_facet |
Інформатика та кібернетика |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/4138 |
| citation_txt |
Производные правила секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2008. — № 4. — С. 51-54. — Бібліогр.: 2 назв. — рос. |
| work_keys_str_mv |
AT pynʹkoap proizvodnyepravilasekvencialʹnyhisčislenijdlâkonečnoznačnyhlogiksopredelitelemravenstva |
| first_indexed |
2025-07-02T07:21:49Z |
| last_indexed |
2025-07-02T07:21:49Z |
| _version_ |
1836518903016062976 |
| 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
|