Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства
Запропоновано ефективну процедуру мінімізації числа засновків правил введення секвенційних числень для пропозиційних скінченнозначних логік з визначником рівності. An effective procedure of minimization of the number of premises for the introduction rules of sequent calculi for propositional finitel...
Збережено в:
| Опубліковано в: : | Доповіді НАН України |
|---|---|
| Дата: | 2011 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Видавничий дім "Академперіодика" НАН України
2011
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/38682 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2011. — № 9. — С. 36-41. — Бібліогр.: 7 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859950956720947200 |
|---|---|
| author | Пынько, А.П. |
| author_facet | Пынько, А.П. |
| citation_txt | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2011. — № 9. — С. 36-41. — Бібліогр.: 7 назв. — рос. |
| collection | DSpace DC |
| container_title | Доповіді НАН України |
| description | Запропоновано ефективну процедуру мінімізації числа засновків правил введення секвенційних числень для пропозиційних скінченнозначних логік з визначником рівності.
An effective procedure of minimization of the number of premises for the introduction rules of sequent calculi for propositional finitely-valued logics with equality determinant is proposed.
|
| first_indexed | 2025-12-07T16:17:03Z |
| format | Article |
| fulltext |
УДК 510.6
© 2011
А.П. Пынько
Оптимизация секвенциальных исчислений
для конечнозначных логик с определителем равенства
(Представлено академиком НАН Украины А.А. Летичевским)
Запропоновано ефективну процедуру мiнiмiзацiї числа засновкiв правил введення секвен-
цiйних числень для пропозицiйних скiнченнозначних логiк з визначником рiвностi.
В данной работе мы предлагаем эффективную процедуру минимазации числа посылок пра-
вил секвенциальных исчислений для конечнозначных логик с определителем равенства,
введенных в работе [1]. Важность указанной минимизации объясняется тем, что мощность
деревьев вывода секвенций в таких исчислениях, которая, в свою очередь, предопреде-
ляет вычислительную сложность процедур поиска вывода, найденных в работе [1], имеет
верхнюю достижимую оценку N∂(Φ), где N — максимальное число посылок правил рас-
сматриваемого исчисления, а ∂(Φ) — степень заданной секвенции Φ (которая определяется
связками, входящими в эту секвенцию). Учитывая определение 1 [1], данная минимизация
эквивалентна минимизации значений компонентов секвенциальных таблиц для рассматри-
ваемых логик, чему и посвящается основная часть данной работы.
Мы следуем терминологии, обозначениям и установкам, принятым в работе [1], за исклю-
чением того, что для простоты изложения секвенции считаются парами конечных множеств
(а не последовательностей) формул, при этом отношение включения ⊆ распространяется на
секвенции покомпонентно. Кроме того, мы полагаем k = l = 0 и, соответственно, опускаем
какое-либо упоминание о ранге.
Пусть F ⊆ FmL. Под (пропозициональными) F -секвенциями мы понимаем пары вида
Γ ⊢ ∆, где Γ, ∆ ⊆ ωF . Секвенция Γ ⊢ ∆ называется рефлексивной, если Γ
⋂
∆ 6= ∅.
Множество всех (иррефлексивных) F -секвенций обозначается Seq(F ) (S̃eq(F )). Следующие
секвенциальные правила называются структурными F -правилами:
сечение
Γ ⊢ ∆
⋃
{ϕ}{ϕ}
⋃
Θ ⊢ Ξ
Γ
⋃
Θ ⊢ ∆
⋃
Ξ
,
утончение
Γ ⊢ ∆
Γ
⋃
Θ ⊢ ∆
⋃
Ξ
,
где ϕ ∈ F , Γ, ∆, Θ, Ξ ⊆ ωF .
Пусть 〈P,6〉 — частично упорядоченное множество и B ⊆ P . Множество всех минималь-
ных относительно 6 элементов B обозначается Min6(B). Положим B↑6 := {a ∈ P | ∃ b ∈
∈ B : b 6 a}. Далее, B называется антицепью (верхним конусом) 〈P,6〉, если Min6(B) = B
(B↑6 = B). Две антицепи частично упорядоченного множества 〈P,6〉 называются несрав-
нимыми, если их объединение само является антицепью 〈P,6〉, а пересечение пусто.
Для произвольных Γ, ∆ ⊆ SeqL полагаем Γ ≡ M∆ ⇐⇒ CnM(Γ) = CnM(∆). Для
произвольных Φ, Ψ ∈ SeqL полагаем Φ ⊳M Ψ ⇐⇒ Ψ ∈ CnM(Φ). При этом, ⊳M является
36 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2011, №9
отношением квазиупорядочения, а ≡ M
⋂
Seq2L = ⊳M
⋂
⊳−1
M
— отношением эквивалентности
на SeqL.
В силу равенств (1) и (2), а также конструктивного доказательства теоремы 1 рабо-
ты [2], задача построения секвенциальной таблицы для всех элементов M с минимальными
значениями ее компонентов сводится к более общей задаче вычисления, для произвольных
n > 0 и S ⊆ S̃eq(ℑ({p1, . . . , pn})), конечного множества S ≡ MT ⊆ S̃eq(ℑ({p1, . . . , pn}))
с минимальным числом элементов. Данная задача аналогична задаче построения кратчай-
шей дизъюнктивной нормальной формы (д. н.ф.) в алгебре логики [3]. Более того, если
M = {M}, а M — двузначна, поставленная задача эквивалентна вышеуказанной задаче те-
ории булевых функций. Поэтому мы используем идеи построения минимальной д. н.ф. [3],
которое отличается от построения кратчайшей д. н.ф. только заключительным перебором
очевидным образом.
Зафиксируем n > 0. Положим
Axm: = {Φ[σ] | Φ ∈ Âx(p1, . . . , pm), σ : {p1, . . . , pm} → {p1, . . . , pn}},
Ãxm := Axm
⋂
S̃eq(ℑ({p1, . . . , pn})).
Заметим, что
Seq(ℑ({p1, . . . , pn})) \ S̃eq(ℑ({p1, . . . , pn})) ⊆ Axm↑⊆, (1)
S ≡ MS \ Axm↑⊆, (2)
где S ⊆ Seq(ℑ({p1, . . . , pn})).
Пусть S ⊆ S̃eq(ℑ({p1, . . . , pn})). Рассмотрим процедуру, состоящую из следующих ша-
гов:
1) вычисляем конечное множество
M(S) := Min⊆(CnM(S)
⋂
Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆);
2) разбиваем M(S) на классы эквивалентности по отношению ≡ M и выбираем по одно-
му элементу из каждого, получая в результате множество P(S), частично упорядоченное
отношением ⊳M;
3) вычисляем множество Q(S) := Min⊳M(P(S));
4) вычисляем множество K(S) := {Φ ∈ Q(S) | Φ 6∈ CnM(Q(S) \ {Φ});
5) вычисляем множество R(S) := Q(S) \ CnM(K(S));
6) для каждого 0 6 i 6 |R(S)| и H ⊆ R(S) с |H| = i проверяем включение R(S) \H ⊆
⊆ CnM(K(S)
⋃
H) и при первом позитивном ответе завершаем процедуру, положив T(S) :=
= K(S)
⋃
H.
Отметим, что если M = {M}, а M — двузначна, то Φ ⊳M Ψ ⇐⇒ Φ ⊆ Ψ и Φ ≡
≡ MΨ ⇐⇒ Φ = Ψ для всех Φ, Ψ ∈ S̃eq(ℑ({p1, . . . , pn})). В этом случае, с учетом (1),
Q(S) = P(S) = M(S).
Предложение 1. Для произвольного S ⊆ S̃eq(ℑ({p1, . . . , pn})):
S ≡ MT(S) ⊆ S̃eq(ℑ({p1, . . . , pn})),
|T(S)| = min{|T | | S ≡ MT ⊆ S̃eq(ℑ({p1, . . . , pn}))}.
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2011, №9 37
Доказательство. В силу конечности множества Seq(ℑ({p1, . . . , pn})) всякая секвенция
Φ ∈ CnM(S)
⋂
Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆ имеет Φ ⊲M Ψ ∈ Q(S). Поэтому всякое S ≡
≡ MX ⊆ Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆ имеет X ≡ MY ⊆ Q(S) с |Y | = |X|. С учетом (1)
и (2) дальнейшая аргументация очевидна.
Шаги 2–6 вышеприведенной процедуры реализуются непосредственно. При этом про-
верка условий вида Φ ∈ CnM(Γ), где Φ ∈ S̃eq(ℑ({p1, . . . , pn})) и Γ ⊆ S̃eq(ℑ({p1, . . . , pn})),
может осуществляться как алгебраически, так и дедуктивно — с использованием теоремы
сильной полноты работы [4] (см. теорему 1 и замечание 1 цитируемой работы) и предло-
женных в ней программных средств. Что касается шага 1, его непосредственная реализа-
ция требует перебора всех пар элементов множества CnM(S)
⋂
Seq(ℑ({p1, . . . , pn}))\Axm↑⊆.
Например, в случае трех- и четырехзначных логик с конструктивным отрицанием (см. при-
мер 2 работы [2]), когда |ℑ| = 2, и бинарной связки число таких пар может достигать 216.
Цель остальной части настоящей работы — найти способ вычисления множества M(S) без
вышеуказанного перебора. Ключевым средством эффективной реализации шага 1 является
вышеупомянутая теорема сильной полноты [4].
Лемма 1. Для произвольных Σ ∈ Seq(ℑ({p1, . . . , pn})) и S ⊆ Seq(ℑ({p1, . . . , pn})), Σ ∈
∈ CnM(S) тогда и только тогда, когда Σ выводима из S
⋃
Axm с помощью структурных
ℑ({p1, . . . , pn})-правил.
Доказательство. По теореме сильной полноты работы [4] (см. теорему 1 и замечание 1
цитируемой работы), при L′ = ∅ и W = {p1, . . . , pn}.
Для произвольных Γ, ∆, Θ, Ξ ⊆ ωFmL положим
Cut(Γ ⊢ ∆,Θ ⊢ Ξ) := {Γ
⋃
(Θ \ {ϕ}) ⊢ (∆ \ {ϕ})
⋃
Ξ | ϕ ∈ ∆
⋂
Θ}.
Далее, для произвольного G ⊆ Seq(ℑ({p1, . . . , pn}))
2 полагаем
Cut(G) :=
⋃
{Cut(Φ,Ψ) | 〈Φ,Φ〉 ∈ G}.
Определим оператор ℜ+ на верхних конусах 〈Seq(ℑ({p1, . . . , pn})),⊆〉, включающих Axm:
ℜ+(U) := U
⋃
Cut(U2)↑⊆,
где U — верхний конус 〈Seq(ℑ({p1, . . . , pn})),⊆〉, включающий Axm. Далее определим опе-
ратор ℜ− на антицепях 〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉:
ℜ−(C) := Min⊆(C
⋃
(Cut(C2
⋃
(C ×Min⊆(Ãxm))
⋃
(Min⊆(Ãxm)× C)) \Axm↑⊆)),
где C — антицепь 〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉. И, наконец, определим оператор ℜ на
парах несравнимых антицепей 〈Seq(ℑ({p1, . . . , pn})) \Axm↑⊆⊆:
π0(ℜ(C0, C1)) := Min⊆(Cut(C
2
0
⋃
(C0 × (C1
⋃
Min⊆(Ãxm)))
⋃
⋃
((C1
⋃
Min⊆(Ãxm))× C0)) \ (C0
⋃
C1
⋃
Axm)↑⊆),
π1(ℜ(C0, C1)) := (C0
⋃
C1) \ π0(ℜ(C0, C1))↑⊆,
где 〈C0, C1〉 — пара несравнимых антицепей 〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉.
Замечание 1. Отображения
f : U 7→ Min⊆(U \Axm↑⊆), g : C 7→ (C
⋃
Axm)↑⊆,
38 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2011, №9
где U — верхний конус 〈Seq(ℑ({p1, . . . , pn})),⊆〉, включающий Axm, а C — антицепь час-
тично упорядоченного множества 〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉, образуют взаимно од-
нозначное соответствие между множествами всех верхних конусов 〈Seq(ℑ({p1, . . . , pn})),⊆〉,
включающих Axm, и всех антицепей 〈Seq(ℑ({p1, . . . , pn})) \Axm↑⊆,⊆〉.
Лемма 2. g(ℜ−(C)) = ℜ+(g(C)) для любой антицепи C частично упорядоченного мно-
жества 〈Seq(ℑ({p1, . . . , pn})) \Axm↑⊆,⊆〉.
Доказательство. Включение g(ℜ−(C)) ⊆ ℜ+(g(C)) доказывается непосредственно.
Для доказательства обратного возьмем произвольную Σ ∈ ℜ+(g(C)). Рассмотрим следую-
щие два случая:
1) Σ ∈ Axm↑⊆.
Тогда, Σ ∈ g(ℜ−(C));
2) Σ 6∈ Axm↑⊆.
Рассмотрим следующие два случая:
а)Σ ∈ g(C).
Тогда, Σ ∈ C↑⊆. Поэтому, существует такая Σ′ ∈ C, что Σ′ ⊆ Σ. Тем самым, существует
такая Σ′′ ∈ ℜ−(C), что Σ′′ ⊆ Σ′. Поэтому, Σ ∈ g(ℜ−(C));
б) Σ 6∈ g(C).
Тогда существует такая Σ′ ∈ Cut(g(C)2), что Σ′ ⊆ Σ. Поэтому существуют такие Φ,
Ψ ∈ g(C), что Σ′ ∈ Cut(Φ,Ψ). Применяя теорему 1 [1] при L′ = ∅ и W = {p1, . . . , pn},
получаем Axm↑⊆ = CnM(∅)
⋂
Seq(ℑ({p1, . . . , pn})). Поскольку данное множество замкну-
то относительно сечений, {Φ,Ψ} 6⊆ Axm↑⊆. Пусть Φ = Γ ⊢ ∆, Ψ = Θ ⊢ Ξ и Σ′ =
= Γ
⋃
(Θ\{ϕ}) ⊢ (∆\{ϕ})
⋃
Ξ, где ϕ ∈ ∆
⋂
Θ. Учитывая (1), Σ и, следовательно, Σ′ иррефле-
ксивна. От противного докажем, что как Φ, так и Ψ также иррефлексивны. Предположим,
что одна из данных секвенций (без ограничения общности можно считать, что Φ) рефлек-
сивна. Тогда, в силу иррефлексивности Σ′, ϕ ∈ Γ и, тем самым, Ψ ⊆ Σ, что противоречит
тому, что Σ 6∈ g(C). Таким образом, Φ и Ψ иррефлексивны. Поэтому существуют такие
Φ′ = Γ′ ⊢ ∆′ ⊆ Φ и Ψ′ = Θ′ ⊢ Ξ′ ⊆ Ψ, что 〈Φ′,Φ′〉 ∈ C2⋃(C×Min⊆(Ãxm))
⋃
(Min⊆(Ãxm)×C).
От противного докажем, что ϕ ∈ ∆′
⋂
Θ′. Предположим, что ϕ 6∈ ∆′
⋂
Θ′. Без ограничения
общности можно считать, что ϕ 6∈ ∆′. Тогда Φ′ ⊆ Σ, что противоречит тому, что Σ 6∈ g(C).
Таким образом, ϕ ∈ ∆′
⋂
Θ′. Тогда Σ ⊇ Γ′
⋃
(Θ′ \ {ϕ}) ⊢ (∆′ \ {ϕ})
⋃
Ξ′ ∈ g(ℜ−(C)) и, тем
самым, Σ ∈ g(ℜ−(C)).
Лемма 3. Для любого i ∈ ω и любой антицепи C частично упорядоченного множества
〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉, Cut(π1(ℜ
i(〈C,∅〉))2
⋃
(π1(ℜ
i(〈C,∅〉)) × Min⊆(Ãxm))
⋃
⋃
(Min⊆(Ãxm) × π1(ℜ
i(〈C,∅〉)))) ⊆ (π0(ℜ
i(〈C,∅〉))
⋃
π1(ℜ
i(〈C,∅〉))
⋃
Axm)↑⊆.
Доказательство. Индукцией по i. При i = 0 утверждение леммы очевидно. Предпо-
ложим, что оно верно при i = j ∈ ω. Докажем его истинность при i = j + 1. Положим
M := Min⊆(Ãxm) и Cr
s := πs(ℜ
r(〈C,∅〉)), где r ∈ {j, j + 1} и s ∈ 2. Заметим, что C
j+1
1 ⊆
⊆ C
j
0
⋃
C
j
1 . Кроме того, для любого частично упорядоченного множества 〈P,6〉 и любых
E, B ⊆ P , E↑6 \B↑6 ⊆ (E \B↑6)↑6. Поэтому, учитывая индукционное предположение, мы
имеем Cut((Cj+1
1 )2
⋃
(Cj+1
1 ×M)
⋃
(M ×C
j+1
1 )) ⊆ Cut((Cj
0)
2
⋃
(Cj
0 × (Cj
1
⋃
M))
⋃
((Cj
1
⋃
M)×
×C
j
0))
⋃
(Cj
0
⋃
C
j
1
⋃
Axm)↑⊆ ⊆ C
j+1
0 ↑⊆
⋃
(Cj
0
⋃
C
j
1)↑⊆
⋃
Axm↑⊆ ⊆ C
j+1
0 ↑⊆
⋃
C
j+1
1 ↑⊆
⋃
Axm↑⊆.
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2011, №9 39
Лемма 4. Для любого i ∈ ω и любой антицепи C частично упорядоченного множества
〈Seq(ℑ({p1, . . . , pn})) \ Axm↑⊆,⊆〉,
ℜi+1(〈C,∅〉) = 〈ℜi+1
− (C) \ ℜi
−(C),ℜi+1
− (C)
⋂
ℜi
−(C)〉. (3)
Доказательство. Путем доказательства индукцией по j ∈ ω того факта, что
π0(ℜ
j(〈C,∅〉))
⋃
π1(ℜ
j(〈C,∅〉)) = ℜj
−(C). (4)
При j = 0 равенство (4) очевидно. Предположим, что (4) верно при j = i. Докажем
истинность (4) при j = i + 1. По лемме 3 и индукционному предположению мы имеем
ℜi+1(〈C,∅〉) = ℜ(〈π0(ℜ
i(〈C,∅〉))
⋃
π1(ℜ
i(〈C,∅〉)),∅〉) = ℜ(〈ℜi
−(C),∅〉). Кроме того, непо-
средственной проверкой нетрудно убедиться в том, что для любого частично упорядочен-
ного множества 〈P,6〉, любой его антицепи E и любых H, B ⊆ P , Min6(B \ (E
⋃
H)↑6) =
= Min6(E
⋃
(B \H↑6)) \E и E \ (B \ (E
⋃
H)↑6)↑6 = Min6(E
⋃
(B \H↑6))
⋂
E. Тем самым,
мы получаем (3), что непосредственно дает (4) при j = i + 1.
Лемма 5. Для любого верхнего конуса U ⊇ Axm частично упорядоченного множества
〈Seq(ℑ({p1, . . . , pn})),⊆〉 существует такое j ∈ ω, что ℜj+1
+ (U) = ℜj
+(U) = CnM(U)
⋂
⋂
Seq(ℑ({p1, . . . , pn})).
Доказательство. Так как множество Seq(ℑ({p1, . . . , pn})) конечно и U ⊆ ℜ+(U), су-
ществует такое j ∈ ω, что ℜj+1
+ (U) = ℜj
+(U). При этом U
⋃
Axm ⊆ ℜj
+(U), а ℜj
+(U) замкну-
то относительно структурных ℑ({p1, . . . , pn})-правил. С другой стороны, всякий элемент
ℜj
+(U) выводим из U с помощью структурных ℑ({p1, . . . , pn})-правил. Тем самым лемма 1
завершает доказательство.
Из замечания 1 и лемм 2, 4 и 5 непосредственно вытекает
Теорема 1. Для любого S ⊆ S̃eq(ℑ({p1, . . . , pn})) существует такое (наименьшее) j ∈
∈ ω, что π0(ℜ
j(〈Min⊆(S \Axm↑⊆),∅〉)) = ∅. При этом π1(ℜ
j(〈Min⊆(S \Axm↑⊆),∅〉)) =
= M(S).
Вычислительные эксперименты, проведенные в системе SWI-Prolog для различных изве-
стных многозначных логик, показали, что вычисления с использованием оператора ℜ в со-
ответствии с теоремой 1 примерно на два порядка эффективнее, чем при непосредственном
вычислении множества M(S), что оправдывает вышеизложенную разработку. Примеча-
тельным является также то, что во всех рассмотренных примерах множество R(S) ока-
зывалось пустым, что полностью исключало перебор на шаге 6 вышеописанной процедуры
и делало ее шаг 1 настолько критическим в плане ее вычислительной сложности. Это де-
монстрирует адекватность вычислительной стратегии, предложенной в настоящей работе
и, кроме того, объясняет тот любопытный факт, что исчисления, полученные с помощью
нашей процедуры, совпали с теми, которые были найдены ранее эвристическим путем, ведь
T(S) определяется однозначно при R(S) = ∅, а выбор минимального исчисления естестве-
нен с исследовательской точки зрения.
Предложение 1 и теорема 1 дают не только вычислительное средство минимизации пра-
вил исчислений для многозначных логик, но и методику эвристического доказательства
минимальности правил заданного исчисления. Например, когда M = {M}, а M — класси-
ческая логика, для секвенциальной таблицы, соответствующей исчислению Генцена [5, 6],
имеют место равенства T(S) = K(S) = Q(S) = P(S) = M(S) = S и R(S) = ∅. Тем самым,
исчисление Генцена оптимально. Аналогичная ситуация имеет место для четырехзначных
логик и исчислений, рассмотренных в работе [7].
40 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2011, №9
1. Пынько А.П. Процедуры вывода в секвенциальных исчислениях для конечнозначных логик с опре-
делителем равенства // Доп. НАН України. – 2007. – № 3. – С. 45–51.
2. Пынько А.П. Секвенциальные исчисления для конечнозначных логик с определителем равенства //
Там само. – 2003. – № 8. – С. 69–75.
3. Яблонский С.В. Введение в дискретную математику. – Москва: Наука, 1986. – 384 с.
4. Пынько А.П. Производные правила секвенциальных исчислений для конечнозначных логик с опре-
делителем равенства // Доп. НАН України. – 2008. – № 4. – С. 51–54.
5. Gentzen G. Untersuchungen über das logische Schließen (I) // Math. Zeit. – 1934. – 39. – P. 176–210.
6. Gentzen G. Untersuchungen über das logische Schließen (II) // Ibid. – P. 405–431.
7. Pynko A.P. Functional completeness and axiomatizability within Belnap’s four-valued logic and its expan-
sions // J. of Appl. Non-Classical Logics. – 1999. – 9, No 1. – P. 61–105.
Поступило в редакцию 10.12.2010Институт кибернетики им. В.М. Глушкова
НАН Украины, Киев
A.P. Pynko
Optimization of sequent calculi for finitely-valued logics with equality
determinant
An effective procedure of minimization of the number of premises for the introduction rules of
sequent calculi for propositional finitely-valued logics with equality determinant is proposed.
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2011, №9 41
|
| id | nasplib_isofts_kiev_ua-123456789-38682 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1025-6415 |
| language | Russian |
| last_indexed | 2025-12-07T16:17:03Z |
| publishDate | 2011 |
| publisher | Видавничий дім "Академперіодика" НАН України |
| record_format | dspace |
| spelling | Пынько, А.П. 2012-11-19T12:13:28Z 2012-11-19T12:13:28Z 2011 Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства / А.П. Пынько // Доп. НАН України. — 2011. — № 9. — С. 36-41. — Бібліогр.: 7 назв. — рос. 1025-6415 https://nasplib.isofts.kiev.ua/handle/123456789/38682 510.6 Запропоновано ефективну процедуру мінімізації числа засновків правил введення секвенційних числень для пропозиційних скінченнозначних логік з визначником рівності. An effective procedure of minimization of the number of premises for the introduction rules of sequent calculi for propositional finitely-valued logics with equality determinant is proposed. ru Видавничий дім "Академперіодика" НАН України Доповіді НАН України Інформатика та кібернетика Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства Optimization of sequent calculi for finitely-valued logics with equality determinant Article published earlier |
| spellingShingle | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства Пынько, А.П. Інформатика та кібернетика |
| title | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_alt | Optimization of sequent calculi for finitely-valued logics with equality determinant |
| title_full | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_fullStr | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_full_unstemmed | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_short | Оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| title_sort | оптимизация секвенциальных исчислений для конечнозначных логик с определителем равенства |
| topic | Інформатика та кібернетика |
| topic_facet | Інформатика та кібернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/38682 |
| work_keys_str_mv | AT pynʹkoap optimizaciâsekvencialʹnyhisčisleniidlâkonečnoznačnyhlogiksopredelitelemravenstva AT pynʹkoap optimizationofsequentcalculiforfinitelyvaluedlogicswithequalitydeterminant |