Конъюнктивная нормальная форма

Не путать с нормальной формой Хомского .

В булевой логике формула если находится в конъюнктивной нормальной форме ( CNF ) или форме, она представляет собой соединение одного или нескольких предложений , где предложение является дизъюнкцией литералов ; клаузальной нормальной иначе говоря, это произведение сумм или И из ИЛИ . Как каноническая нормальная форма , она полезна в автоматизированном доказательстве теорем и теории цепей .

В автоматизированном доказательстве теорем понятие « клаузальная нормальная форма » часто используется в более узком смысле, означая конкретное представление формулы КНФ в виде набора наборов литералов.

Определение

Логическая формула считается находящейся в КНФ, если она представляет собой конъюнкцию одной или нескольких дизъюнкций одного или нескольких литералов . Как и в дизъюнктивной нормальной форме (ДНФ), единственными пропозициональными операторами в КНФ являются или ( $\vee$), и ( $\wedge$), и не ( $\neg$). Оператор not может использоваться только как часть литерала, то есть он может предшествовать только пропозициональной переменной .

Ниже приведена контекстно-свободная грамматика для CNF:

1. CNF → ( Дизъюнкция ) $\land$ КНФ
2. CNF → ( Дизъюнкция )
3. Дизъюнкция → Буквальный $\lor$ Дизъюнкция
4. Дизъюнкция → Буквальный
5. Буквальный → $\neg$Переменная
6. Литерал → Переменная

Где Variable — любая переменная.

Все следующие формулы в переменных $A,B,C,D,E$, и $F$ находятся в конъюнктивной нормальной форме:

• $(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F\lor D\lor F)$
• $(A\lor B)\land (C)$
• $(A\lor B)$
• $(A)$

Следующие формулы не находятся в конъюнктивной нормальной форме:

• $\neg (A\land B)$, поскольку оператор AND вложен в оператор NOT
• $\neg (A\lor B)\land C$, поскольку оператор OR вложен в оператор NOT
• $A\land (B\lor (D\land E))$, поскольку оператор AND вложен в оператор OR

Преобразование в CNF

В классической логике каждую пропозициональную формулу можно преобразовать в эквивалентную формулу в КНФ. Это преобразование основано на правилах логической эквивалентности : исключении двойного отрицания , законах Де Моргана и распределительном законе .

Основной алгоритм

Алгоритм вычисления КНФ-эквивалента заданной пропозициональной формулы $\phi$ опирается на $\lnot \phi$ в дизъюнктивной нормальной форме (ДНФ) : шаг 1.
Затем $\lnot \phi _{DNF}$ преобразуется в $\phi _{CNF}$заменяя AND на OR и наоборот, отрицая при этом все литералы. Убрать все $\lnot \lnot$.

Преобразование синтаксическими средствами

Преобразуйте в КНФ пропозициональную формулу $\phi$.

Шаг 1 : Преобразуйте его отрицание в дизъюнктивную нормальную форму.

$\lnot \phi _{DNF}=(C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})$,

где каждый $C_{i}$ это соединение литералов $l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}}$.

Шаг 2 : Отрицание $\lnot \phi _{DNF}$. Затем сдвиньте $\lnot$ внутрь, применяя (обобщенные) эквивалентности Де Моргана до тех пор, пока это становится невозможным.

$${\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot (C_{1}\lor C_{2}\lor \ldots \lor C_{i}\lor \ldots \lor C_{m})\\&\leftrightarrow \lnot C_{1}\land \lnot C_{2}\land \ldots \land \lnot C_{i}\land \ldots \land \lnot C_{m}&&{\text{// (generalized) D.M.}}\end{aligned}}$$

где

$${\begin{aligned}\lnot C_{i}&=\lnot (l_{i1}\land l_{i2}\land \ldots \land l_{in_{i}})\\&\leftrightarrow (\lnot l_{i1}\lor \lnot l_{i2}\lor \ldots \lor \lnot l_{in_{i}})&&{\text{// (generalized) D.M.}}\end{aligned}}$$

Шаг 3 : Удалите все двойные отрицания.

Пример

Преобразуйте в КНФ пропозициональную формулу $\phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))$.

(Полный) ДНФ-эквивалент его отрицания:
$\lnot \phi _{DNF}=(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)$

$${\begin{aligned}\phi &\leftrightarrow \lnot \lnot \phi _{DNF}\\&=\lnot \{(p\land q\land r)\lor (p\land q\land \lnot r)\lor (p\land \lnot q\land \lnot r)\lor (\lnot p\land q\land \lnot r)\}\\&\leftrightarrow {\underline {\lnot (p\land q\land r)}}\land {\underline {\lnot (p\land q\land \lnot r)}}\land {\underline {\lnot (p\land \lnot q\land \lnot r)}}\land {\underline {\lnot (\lnot p\land q\land \lnot r)}}&&{\text{// generalized D.M. }}\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor \lnot \lnot r)\land (\lnot p\lor \lnot \lnot q\lor \lnot \lnot r)\land (\lnot \lnot p\lor \lnot q\lor \lnot \lnot r)&&{\text{// generalized D.M. }}(4\times )\\&\leftrightarrow (\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)&&{\text{// remove all }}\lnot \lnot \\&=\phi _{CNF}\end{aligned}}$$

Преобразование семантическими средствами

Эквивалент формулы в CNF может быть получен из ее таблицы истинности . Еще раз рассмотрим формулу

$$\phi =((\lnot (p\land q))\leftrightarrow (\lnot r\uparrow (p\oplus q)))$$

.

Соответствующая таблица истинности

$p$	$q$	$r$		$($	$\lnot$	$(p\land q)$	$)$	$\leftrightarrow$	$($	$\lnot r$	$\uparrow$	$(p\oplus q)$	$)$
Т	Т	Т			Ф	Т		Ф		Ф	Т	Ф
Т	Т	Ф			Ф	Т		Ф		Т	Т	Ф
Т	Ф	Т			Т	Ф		Т		Ф	Т	Т
Т	Ф	Ф			Т	Ф		Ф		Т	Ф	Т
Ф	Т	Т			Т	Ф		Т		Ф	Т	Т
Ф	Т	Ф			Т	Ф		Ф		Т	Ф	Т
Ф	Ф	Т			Т	Ф		Т		Ф	Т	Ф
Ф	Ф	Ф			Т	Ф		Т		Т	Т	Ф

CNF-эквивалент $\phi$ является

$$(\lnot p\lor \lnot q\lor \lnot r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor q\lor r)\land (p\lor \lnot q\lor r)$$

Каждая дизъюнкция отражает присвоение переменных, для которых $\phi$ оценивается как F(alse).
Если в таком присваивании переменная $V$

• равно T(rue), то литералу присваивается значение $\lnot V$ в дизъюнкции,
• равно F(alse), то литералу присваивается значение $V$ в дизъюнкции.

Другие подходы

Поскольку все пропозициональные формулы можно преобразовать в эквивалентную формулу в конъюнктивной нормальной форме, доказательства часто основаны на предположении, что все формулы являются КНФ. Однако в некоторых случаях это преобразование в CNF может привести к экспоненциальному взрыву формулы. Например, перевод формулы, отличной от CNF

$$(X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \ldots \vee (X_{n}\wedge Y_{n})$$

в CNF создает формулу с $2^{n}$ положения:

$$(X_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \ldots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \ldots \vee X_{n})\wedge \ldots \wedge (Y_{1}\vee Y_{2}\vee \ldots \vee Y_{n}).$$

Каждое предложение содержит либо $X_{i}$ или $Y_{i}$ для каждого $i$.

Существуют преобразования в КНФ, которые избегают экспоненциального увеличения размера, сохраняя выполнимость , а не эквивалентность . Эти преобразования гарантированно только линейно увеличивают размер формулы, но вводят новые переменные. Например, приведенную выше формулу можно преобразовать в КНФ, добавив переменные $Z_{1},\ldots ,Z_{n}$ следующее:

$$(Z_{1}\vee \ldots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \ldots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).$$

Интерпретация удовлетворяет этой формуле только в том случае , если хотя бы одна из новых переменных верна. Если эта переменная $Z_{i}$, то оба $X_{i}$ и $Y_{i}$также верны. Это означает, что каждая модель , удовлетворяющая этой формуле, также удовлетворяет исходной. С другой стороны, этому удовлетворяют лишь некоторые модели исходной формулы: поскольку $Z_{i}$не упоминаются в исходной формуле, их значения не имеют отношения к ее удовлетворению, чего нет в последней формуле. Это означает, что исходная формула и результат перевода равновыполнимы, но не эквивалентны .

Альтернативный перевод — преобразование Цейтина — включает в себя также придаточные предложения $Z_{i}\vee \neg X_{i}\vee \neg Y_{i}$. С учетом этих положений формула подразумевает $Z_{i}\equiv X_{i}\wedge Y_{i}$; эта формула часто считается «определяющей» $Z_{i}$ быть именем для $X_{i}\wedge Y_{i}$.

Максимальное количество дизъюнкций

Рассмотрим пропозициональную формулу с $n$ переменные, $n\geq 1$.

Есть $2n$ возможные литералы: $L=\{p_{1},\lnot p_{1},p_{2},\lnot p_{2},\ldots ,p_{n},\lnot p_{n}\}$.

$L$ имеет $(2^{2n}-1)$ непустые подмножества.

Это максимальное количество дизъюнкций, которое может иметь КНФ.

Все комбинации истинностных функций могут быть выражены с помощью $2^{n}$ дизъюнкции, по одной на каждую строку таблицы истинности.
В примере ниже они подчеркнуты.

Пример

Рассмотрим формулу с двумя переменными $p$ и $q$.

Самый длинный возможный CNF имеет $2^{(2\times 2)}-1=15$ дизъюнкции:

$${\begin{array}{lcl}(\lnot p)\land (p)\land (\lnot q)\land (q)\land \\(\lnot p\lor p)\land {\underline {(\lnot p\lor \lnot q)}}\land {\underline {(\lnot p\lor q)}}\land {\underline {(p\lor \lnot q)}}\land {\underline {(p\lor q)}}\land (\lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q)\land (\lnot p\lor p\lor q)\land (\lnot p\lor \lnot q\lor q)\land (p\lor \lnot q\lor q)\land \\(\lnot p\lor p\lor \lnot q\lor q)\end{array}}$$

Эта формула противоречит .

Вычислительная сложность

Важный набор проблем вычислительной сложности включает в себя поиск таких присвоений переменным булевой формулы, выраженных в конъюнктивной нормальной форме, чтобы формула была истинной. Проблема k -SAT — это проблема поиска удовлетворяющего назначения булевой формуле, выраженной в КНФ, в которой каждая дизъюнкция содержит не более k переменных. 3-SAT является NP-полной (как и любая другая k задача -SAT с k > 2), тогда как 2-SAT известно, что имеет решения за полиномиальное время . Как следствие, задача преобразования формулы в ДНФ с сохранением выполнимости является NP-трудной ; двойственно , преобразование в CNF с сохранением достоверности также является NP-трудным; следовательно, преобразование с сохранением эквивалентности в DNF или CNF снова является NP-трудным.

Типичные проблемы в этом случае связаны с формулами в «3CNF»: конъюнктивной нормальной форме с не более чем тремя переменными на конъюнкт. Примеры таких формул, встречающиеся на практике, могут быть очень большими, например, со 100 000 переменных и 1 000 000 конъюнктов.

Формула в CNF может быть преобразована в равновыполнимую формулу в « k CNF» (для k ≥3), заменив каждый конъюнкт более чем k переменными. $X_{1}\vee \ldots \vee X_{k}\vee \ldots \vee X_{n}$ двумя союзами $X_{1}\vee \ldots \vee X_{k-1}\vee Z$ и $\neg Z\vee X_{k}\lor \ldots \vee X_{n}$ с Z — новую переменную и повторять столько раз, сколько необходимо.

Логика первого порядка

В логике первого порядка конъюнктивную нормальную форму можно использовать дальше, чтобы получить клаузальную нормальную форму логической формулы, которую затем можно использовать для выполнения разрешения первого порядка . При автоматизированном доказательстве теорем на основе разрешения формула CNF

$($

$l_{11}$

$\lor$

$\ldots$

$\lor$

$l_{1n_{1}}$

$)$

$\land$

$\ldots$

$\land$

$($

$l_{m1}$

$\lor$

$\ldots$

$\lor$

$l_{mn_{m}}$

$)$

, обычно представляют как набор множеств

$\{$

$\{$

$l_{11}$

$,$

$\ldots$

$,$

$l_{1n_{1}}$

$\}$

$,$

$\ldots$

$,$

$\{$

$l_{m1}$

$,$

$\ldots$

$,$

$l_{mn_{m}}$

$\}$

$\}$

.

См. пример ниже.

Преобразование из логики первого порядка

Чтобы преобразовать логику первого порядка в CNF:

1. Привести отрицание к нормальной форме .
   1. Устраните импликации и эквивалентности: повторно замените $P\rightarrow Q$ с $\lnot P\lor Q$; заменять $P\leftrightarrow Q$ с $(P\lor \lnot Q)\land (\lnot P\lor Q)$. В конечном итоге это устранит все случаи $\rightarrow$ и $\leftrightarrow$.
   2. Переместите НОТ внутрь, неоднократно применяя закон Де Моргана . В частности, заменить $\lnot (P\lor Q)$ с $(\lnot P)\land (\lnot Q)$; заменять $\lnot (P\land Q)$ с $(\lnot P)\lor (\lnot Q)$; и заменить $\lnot \lnot P$ с $P$; заменять $\lnot (\forall xP(x))$ с $\exists x\lnot P(x)$; $\lnot (\exists xP(x))$ с $\forall x\lnot P(x)$. После этого $\lnot$ может встречаться только непосредственно перед символом-предикатом.
2. Стандартизируйте переменные
   1. Для таких предложений, как $(\forall xP(x))\lor (\exists xQ(x))$которые дважды используют одно и то же имя переменной, измените имя одной из переменных. Это позволит избежать путаницы при удалении кванторов. Например, $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]$ переименован в $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]$.
3. Сколемизировать высказывание
   1. Переместить кванторы наружу: повторно заменить $P\land (\forall xQ(x))$ с $\forall x(P\land Q(x))$; заменять $P\lor (\forall xQ(x))$ с $\forall x(P\lor Q(x))$; заменять $P\land (\exists xQ(x))$ с $\exists x(P\land Q(x))$; заменять $P\lor (\exists xQ(x))$ с $\exists x(P\lor Q(x))$. Эти замены сохраняют эквивалентность, поскольку предыдущий шаг стандартизации переменных гарантировал, что $x$ не встречается в $P$. После этих замен квантор может встречаться только в начальном префиксе формулы, но никогда внутри $\lnot$, $\land$, или $\lor$.
   2. Повторно заменить $\forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)$ с $\forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))$, где $f$ это новый $n$-арный символ функции, так называемая « функция Скулема ». Это единственный шаг, который сохраняет только выполнимость, а не эквивалентность. Он устраняет все экзистенциальные кванторы.
4. Отбросьте все кванторы универсальности.
5. Распределить OR внутри AND: многократно заменить $P\lor (Q\land R)$ с $(P\lor Q)\land (P\lor R)$.

Пример

Например, формула «Любой, кто любит всех животных, в свою очередь любим кем-то» преобразуется в CNF (а затем в форму предложения в последней строке) следующим образом (выделение редексов правил замены в ${\color {red}{\text{red}}}$):

$\forall x$

$($

$\forall y$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\rightarrow$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

$\forall x$

$($

$\forall y$

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

на 1,1

$\forall x$

$\color {red}\lnot$

$($

${\color {red}{\forall y}}$

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

на 1,1

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$($

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

на 1,2

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$\color {red}\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

на 1,2

$\forall x$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\color {red}\exists$

$\color {red}y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

на 1,2

$\forall x$

$($

$\exists y$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$($

$\color {red}\exists$

$\color {red}z$

$\mathrm {Loves} ($

$z$

$,x)$

$)$

на 2

$\forall x$

$\exists z$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$z$

$,x)$

на 3,1

$\forall x$

${\color {red}{\exists z}}$

$\exists y$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$z$

$,x)$

на 3,1

$\forall x$

${\color {red}{\exists y}}$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

на 3,2

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\land$

$\lnot$

$\mathrm {Loves} (x,$

$f(x)$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

на 4

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$)$

$\color {red}\land$

$($

$\lnot \mathrm {Loves} (x,f(x))$

$\color {red}\lor$

$\mathrm {Loves} (g(x),x)$

$)$

на 5

$\{$

$\{$

$\mathrm {Animal} ($

$f(x)$

$)$

$,$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$\}$

$,$

$\{$

$\lnot \mathrm {Loves} (x,f(x))$

$,$

$\mathrm {Loves} (g(x),x)$

$\}$

$\}$

( пункта представление )

Неформально функция Скулема $g(x)$ можно рассматривать как уступку человеку, которому $x$ любим, в то время как $f(x)$ дает животное (если есть), которое $x$не любит. Третья последняя строка снизу читается как « $x$ не любит животное $f(x)$, или еще $x$ любим $g(x)$" .

Вторая последняя строка сверху, $(\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))$, является КНФ.

См. также

• Алгебраическая нормальная форма
• Двойственность конъюнкции/дизъюнкции
• Дизъюнктивная нормальная форма
• Предложение Хорна . Предложение Хорна представляет собой дизъюнктивное предложение ( дизъюнкция литералов неотрицательным ) не более чем с одним положительным, то есть , литералом.
• Алгоритм Куайна – Маккласки

Ссылки

• Эндрюс, Питер Б. (2013). Введение в математическую логику и теорию типов: к истине через доказательство . ISBN  9401599343 .
• Хаусон, Колин (11 октября 2005 г.) [1997]. Логика с деревьями: введение в символическую логику . Рутледж. ISBN  978-1-134-78550-6 .
• Джексон, Пол; Шеридан, Дэниел (10 мая 2004 г.). «Преобразование форм предложений для логических схем» (PDF) . В Хоосе, Хольгер Х.; Митчелл, Дэвид Г. (ред.). Теория и приложения проверки выполнимости . 7-я Международная конференция по теории и приложениям тестирования выполнимости, SAT . Пересмотренные избранные статьи. Конспекты лекций по информатике. Том. 3542. Ванкувер, Британская Колумбия, Канада: Springer 2005. стр. 183–198. дои : 10.1007/11527695_15 . ISBN  978-3-540-31580-3 .
• Кляйне Бюнинг, Ганс; Леттманн, Теодор (28 августа 1999 г.). Пропозициональная логика: дедукция и алгоритмы . Издательство Кембриджского университета . ISBN  978-0-521-63017-7 .
• Рассел, Стюарт ; Норвиг, Питер , ред. (2010) [1995]. Искусственный интеллект: современный подход (PDF) (3-е изд.). Река Аппер-Седл, Нью-Джерси: Прентис-Холл. ISBN  978-0-13-604259-4 . Архивировано (PDF) из оригинала 31 августа 2017 года.
• Цейтин, Григорий С. (1968). «О сложности вывода в исчислении высказываний» (PDF) . В Слисенко А.О. (ред.). Структуры в конструктивной математике и математической логике, часть II, Семинары по математике (перевод с русского) . Математический институт им. Стеклова. стр. 115–125.
• Уайтситт, Дж. Элдон (24 мая 2012 г.) [1961]. Булева алгебра и ее приложения . Курьерская корпорация. ISBN  978-0-486-15816-7 .

Внешние ссылки

• «Конъюнктивная нормальная форма» , Математическая энциклопедия , EMS Press , 2001 [1994]

• «Java-инструмент для преобразования таблицы истинности в CNF и DNF» . Университет Марбурга . Проверено 31 декабря 2023 г.