Как преобразование пропозициональной логики в разреженную алгебру приводит к элегантному и эффективному дизайну
Делиться
Введение
Если вы когда-либо отвечали за управление сложной бизнес-логикой, вы знаете, какими джунглями могут быть вложенные операторы if-else: в них сложно ориентироваться и легко заблудиться. Когда дело доходит до критически важных задач, например, формальной верификации или проверки выполнимости, многие разработчики прибегают к сложным инструментам, таким как автоматизированные системы доказательства теорем или решатели SMT. Несмотря на свою эффективность, эти подходы могут оказаться избыточными и сложными в реализации. Что, если вам нужен всего лишь простой и понятный механизм правил?
Ключевая идея создания такого лёгкого движка основана на концепции, которую нас учили считать проницательной, но непрактичной: таблицах истинности. Экспоненциальный рост, их фатальный недостаток, делает их непригодными для решения реальных задач. Так нам говорили.
Простое наблюдение меняет все: почти во всех практических случаях «невероятно большая» таблица истинности на самом деле не переполнена информацией; по сути, это замаскированная разреженная матрица .
Такое переосмысление делает таблицы истинности как концептуально понятными, так и вычислительно управляемыми.
В этой статье показано, как превратить эту информацию в лёгкий и мощный механизм правил. Мы проведём вас через все необходимые этапы для создания механизма с нуля. Кроме того, вы можете использовать нашу библиотеку с открытым исходным кодом vector-logic, чтобы начать разрабатывать приложения с первого дня. Это руководство предоставит вам всю необходимую информацию для понимания того, что устроено «под капотом».
Хотя все теоретические основы и математические подробности можно найти в нашей исследовательской работе по алгебре состояний [1], здесь мы сосредоточимся на практическом применении. Давайте засучим рукава и начнём строить!
Краткое напоминание о начальном курсе логики
Таблицы истинности
Начнём с быстрого напоминания: логические формулы — это выражения, построенные на основе булевых переменных и логических коннекторов, таких как И, ИЛИ и НЕ. В реальном мире булевы переменные можно рассматривать как выражение событий (например, «чашка кофе полна», что истинно, если чашка действительно полна, и ложно, если она пуста). Например, формула (f = (x_1 vee x_2)) истинна, если (x_1) истинна, (x_2) истинна, или истинны оба. Мы можем использовать эту структуру для построения полной карты всех возможных реальностей методом прямого перебора — таблицы истинности.
Если использовать 1 для «истины» и 0 для «ложи», таблица для (x_1 vee x_2) будет выглядеть следующим образом:
[ begin{Bmatrix}
x_1 & x_2 & x_1 vee x_2 \ hline
0 и 0 и 0 \
0 и 1 и 1 \
1 и 0 и 1 \
1 и 1 и 1
end{Bmatrix} ]
Всё необходимое для логического вывода закодировано в таблице истинности. Давайте посмотрим на это в действии.
Логический вывод
Рассмотрим классический пример транзитивности импликации. Предположим, мы знаем, что… Кстати, всё, что мы говорим «мы знаем», называется посылкой . Предположим, у нас есть две посылки:
- Если (x_1) истинно, то (x_2) должно быть истинным ((x_1 to x_2))
- Если (x_2) истинно, то (x_3) должно быть истинным ((x_2 to x_3))
Вывод легко угадать: «Если (x_1) истинно, то (x_3) должно быть истинно» ((x_1 to x_3)). Однако мы можем дать формальное доказательство, используя таблицы истинности. Сначала обозначим наши формулы:
[begin{align*}
& f_1 = (x_1 to x_2) && text{предпосылка 1}\
& f_2 = (x_2 to x_3) && text{предпосылка 2}\
& f_3 = (x_1 to x_3) && text{вывод}
end{align*}]
Первым шагом является построение таблицы истинности, охватывающей все комбинации трех базовых переменных (x_1), (x_2) и (x_3):
[begin{align*}
begin{Bmatrix}
x_1 & x_2 & x_3 & f_1 & f_2 & f_3 \ hline
0 и 0 и 0 и 1 и 1 и 1 \
0 и 0 и 1 и 1 и 1 и 1 \
0 и 1 и 0 и 1 и 0 и 1 \
0 и 1 и 1 и 1 и 1 и 1 \
1 и 0 и 0 и 0 и 1 и 0 \
1 и 0 и 1 и 0 и 1 и 1 \
1 и 1 и 0 и 1 и 0 и 0 \
1 и 1 и 1 и 1 и 1 и 1
end{Bmatrix}
end{align*}]
Эта таблица содержит восемь строк, по одной для каждого присвоения значений истинности базовым переменным. Переменные (f_1), (f_2) и (f_3) являются производными , поскольку мы вычисляем их значения непосредственно из переменных (x).
Обратите внимание, насколько велика таблица, даже для этого простого случая!
Следующий шаг — позволить нашим предпосылкам, представленным (f_1) и (f_2), действовать как фильтр реальности. Нам известно, что обе они истинны. Следовательно, любая строка, где либо (f_1), либо (f_2) ложны, представляет собой невозможный сценарий, который следует отбросить.
После применения этого фильтра у нас останется гораздо меньшая таблица:
[begin{align*}
begin{Bmatrix}
x_1 & x_2 & x_3 & f_1 & f_2 & f_3 \ hline
0 и 0 и 0 и 1 и 1 и 1 \
0 и 0 и 1 и 1 и 1 и 1 \
0 и 1 и 1 и 1 и 1 и 1 \
1 и 1 и 1 и 1 и 1 и 1
end{Bmatrix}
end{align*}]
И вот что получилось: во всех оставшихся допустимых сценариях (f_3) истинно. Мы доказали, что (f_3) логически следует из (или вытекает из) (f_1) и (f_2).
Действительно элегантный и интуитивно понятный метод. Так почему бы не использовать его для сложных систем? Ответ кроется в простой математике: всего с тремя переменными у нас было (2^3=8) строк. С 20 переменными их было бы больше миллиона. Если взять 200, количество строк превысит количество атомов в Солнечной системе. Но погодите, наша статья на этом не заканчивается. Мы можем это исправить.
Редкое представление
Основная идея решения проблемы экспоненциально растущих таблиц истинности заключается в компактном представлении, обеспечивающем сжатие без потерь.
Помимо простого сжатия таблиц истинности, нам потребуется эффективный способ выполнения логического вывода. Мы добьёмся этого, введя «векторы состояний», представляющие собой множества состояний (строки таблиц истинности), и применяя для их обработки операции теории множеств, такие как объединение и пересечение.
Сжатая таблица истинности
Сначала вернёмся к формуле (f = (x_1 to x_2)). Определим строки, которые делают формулу истинной. Мы используем символ (sim) для обозначения соответствия между формулой и таблицей её «действительных» значений истинности. В нашем примере с (f) для импликации мы записываем:
[begin{align*}
fquadsimquad
begin{Bmatrix}
x_1 и x_2 \ hline
0 и 0 \
0 и 1 \
1 и 1
end{Bmatrix}
end{align*}]
Обратите внимание, что мы удалили строку ((1, 0)), поскольку она делает (f) недействительной. Что произойдёт с этой таблицей, если мы расширим её, включив в неё третью переменную (x_3), от которой (f) не зависит? Классический подход предполагает удвоение размера таблицы истинности, чтобы учесть, что (x_3) может быть 0 или 1, хотя это не добавляет никакой новой информации о (f):
[begin{align*}
fquadsimquad
begin{Bmatrix}
x_1 & x_2 & x_3 \ hline
0 и 0 и 0 \
0 и 0 и 1 \
0 и 1 и 0 \
0 и 1 и 1 \
1 и 1 и 0 \
1 и 1 и 1
end{Bmatrix}
end{align*}]
Какая расточительность! Неинформативные столбцы можно сжать, и для этого мы вводим тире (–) в качестве подстановочного знака. Это можно представить как логического кота Шрёдингера: переменная существует в суперпозиции 0 и 1 до тех пор, пока ограничение или измерение (в контексте обучения мы называем это «доказательством») не переведут её в определённое состояние, исключая одну из возможностей.
Теперь мы можем представить (f) в множестве (n) переменных без всякого раздувания:
[begin{align*}
fquadsimquad
begin{Bmatrix}
x_1 & x_2 & x_3 & ldots & x_n \ hline
0 & 0 & – & ldots & -\
0 & 1 & – &ldточки & – \
1 и 1 и – &ldots & –
end{Bmatrix}
end{align*}]
Мы можем обобщить это, постулируя, что любая строка, содержащая тире, эквивалентна множеству нескольких строк, полученных всеми возможными заменами нулей и единиц на места тире. Например (попробуйте с карандашом и бумагой!):
[begin{align*}
begin{Bmatrix}
x_1 & x_2 & x_3 \ hline
– & 0 & – \
– и 1 и 1
end{Bmatrix} =
begin{Bmatrix}
x_1 & x_2 & x_3 \ hline
0 и 0 и 0 \
0 и 0 и 1 \
1 и 0 и 0 \
1 и 0 и 1 \
0 и 1 и 1 \
1 и 1 и 1
end{Bmatrix}
end{align*}]
В этом суть разреженного представления. Введём несколько определений для основных операций: замену тире нулями и единицами мы называем расширением . Обратный процесс, в котором мы выявляем закономерности для введения тире, называется сокращением . Простейшая форма сокращения, замена двух строк одной, называется атомарным сокращением .
Алгебра состояний
Теперь давайте придадим этим идеям некоторую структуру.
- Состояние — это единое, полное присвоение значений истинности всем переменным — одна строка в полностью развернутой таблице истинности (например, ((0, 1, 1))).
- Вектор состояний — это множество состояний (представьте его подмножеством таблицы истинности). Логическую формулу теперь можно рассматривать как вектор состояний, содержащий все состояния, которые делают её истинной. Особыми случаями являются пустой вектор состояний (0) и вектор, содержащий все (2^n) возможных состояний, который мы называем тривиальным вектором и обозначаем как (mathbf{t}). (Как мы увидим, это соответствует t-объекту со всеми подстановочными знаками.)
- Строка в компактном представлении вектора состояний (например, ((0, -, 1) )) называется t-объектом . Это наш фундаментальный строительный блок — шаблон, который может представлять одно или несколько состояний.
Концептуально, смещение фокуса с таблиц на множества — критически важный шаг. Вспомните, как мы проводили вывод, используя метод таблиц истинности: мы использовали предпосылки (f_1) и (f_2) в качестве фильтра, оставляя только те строки, где обе предпосылки были истинными. Эта операция, на языке теории множеств, называется пересечением .
Каждой предпосылке соответствует вектор состояния (множество состояний, удовлетворяющих этой предпосылке). Вектор состояния для нашего объединённого знания представляет собой пересечение векторов этих предпосылок. Эта операция лежит в основе новой модели.
Для более удобной записи мы вводим некоторый «синтаксический сахар», сопоставляя операции над множествами с простыми арифметическими операциями:
- Объединение множеств ((cup)) (rightarrow) Сложение ((+))
- Установить Пересечение ((cap)) (rightarrow) Умножение ((*))
Свойства этих операций (ассоциативность, коммутативность и дистрибутивность) позволяют нам использовать обозначения школьной алгебры для сложных выражений с операциями над множествами:
[
begin{align*}
& (Acup B) cap (Ccup D) = (Acup C) cup (Acup D) cup (Bcup C) cup (Bcup D) \
& rightarrow \
& (А+Б)cdot(С+Д) = А,С + А,D + Б,С + Б,D
end{align*}
]
Давайте сделаем перерыв и посмотрим, где мы находимся. Мы заложили прочный фундамент для новой структуры. Таблицы истинности теперь представлены разреженно, и мы интерпретируем их как множества (векторы состояний). Мы также установили, что логический вывод может быть выполнен путём умножения векторов состояний.
Мы почти у цели. Но прежде чем мы сможем применить эту теорию для разработки эффективного алгоритма вывода, нам понадобится ещё один ингредиент. Давайте подробнее рассмотрим операции над t-объектами.
Машинное отделение: Операции на Т-объектах
Теперь мы готовы перейти к следующему этапу — созданию алгебраического движка для эффективной работы с векторами состояния. Основным строительным блоком нашей конструкции является t-объект — компактное представление одной строки вектора состояния с использованием подстановочных знаков.
Обратите внимание, что для описания строки нам достаточно знать только позиции нулей и единиц. Мы обозначаем t-объект как (mathbf{t}^alpha_beta), где (alpha) — множество индексов, где переменная равна 1, а (beta) — множество индексов, где она равна 0. Например:
[
begin{Bmatrix}
x_1 & x_2 & x_3 & x_4 \ hline
1 и 0 и – и 1
end{Bmatrix} = mathbf{t}_2^{14}
]
T-объект, состоящий из всех черточек (mathbf{t} = { -;; – ldots -}), представляет собой ранее упомянутый тривиальный вектор состояний, содержащий все возможные состояния.
От формул к Т-объектам
Вектор состояния представляет собой объединение своих строк или, в нашей новой нотации, сумму своих t-объектов. Мы называем это разложением по строкам . Например, формулу (f=(x_1to x_2)) можно представить как:
[begin{align*}
fquadsimquad
begin{Bmatrix}
x_1 & x_2 & ldots & x_n \ hline
0 & 0 & ldots & -\
0 & 1 & ldots & – \
1 и 1 и ldots & –
end{Bmatrix} = mathbf{t}_{12} + mathbf{t}_1^2 + mathbf{t}^{12}
end{align*}]
Обратите внимание, что это разложение не изменится, если мы добавим в систему больше переменных ((x_3, x_4, dots)), что показывает, что наш подход по своей сути масштабируем.
Правило противоречия
Один и тот же индекс не может присутствовать одновременно в верхней и нижней позициях t-объекта. В этом случае t-объект равен NULL (пустому множеству). Например (мы выделили конфликтующий индекс):
[
mathbf{t}^{1{color{red}3}}_{2{color{red}3}} = 0
]
Это алгебраический эквивалент логического противоречия. Переменная (в данном случае (x_3)) не может быть одновременно истинной (верхний индекс) и ложной (нижний индекс). Любой такой t-объект представляет невозможное состояние и исчезает.
Упрощение выражений: атомарное сокращение
Атомарную редукцию можно выразить ясно, используя новую нотацию t-объекта. Две строки можно редуктировать, если они идентичны, за исключением одной переменной, которая в одной равна 0, а в другой — 1. Например:
[
begin{align*}
begin{Bmatrix}
x_1 & x_2 & x_3 & x_4 & x_5 \ hline
1 & – & 0 & 0 & – \
1 & – & 0 & 1 & –
end{Bmatrix} =
begin{Bmatrix}
x_1 & x_2 & x_3 & x_4 & x_5 \ hline
1 & – & 0 & – & –
end{Bmatrix}
end{align*}
]
В алгебраических терминах это выглядит так:
[
mathbf{t}^1_{34} + mathbf{t}^{14}_3 = mathbf{t}^1_3
]
Правило этой операции непосредственно следует из определения t-объектов: если два t-объекта имеют идентичные наборы индексов, за исключением одного индекса, который в одном случае является надстрочным, а в другом — подстрочным, они объединяются. Конфликтующий индекс (в данном примере 4) уничтожается, и два t-объекта объединяются.
Применив атомарную редукцию, мы можем упростить разложение формулы (f = (x_1 to x_2)). Заметив, что (mathbf{t}_{12} + mathbf{t}_1^2 = mathbf{t}_1), получаем:
[
f quad simquad mathbf{t}_{12} + mathbf{t}_1^2 + mathbf{t}^{12} = mathbf{t}_1 + mathbf{t}^{12}
]
Основная операция: умножение
Наконец, давайте обсудим важнейшую операцию для нашей системы правил: пересечение (в терминах теории множеств), представленное как умножение (в терминах алгебры). Как нам найти состояния, общие для двух t-объектов?
Правило, управляющее этой операцией, простое: чтобы умножить два t-объекта, нужно сформировать объединение их верхних индексов, а также объединение их нижних индексов (доказательство мы оставляем в качестве простого упражнения для любознательного читателя):
[
mathbf{t}^{alpha_1}_{beta_1},mathbf{t}^{alpha_2}_{beta_2} = mathbf{t}^{alpha_1 cup alpha_2}_{beta_1cupbeta_2}
]
Правило противоречия всё ещё действует. Если результирующие наборы надстрочных и подстрочных индексов пересекаются, произведение обращается в ноль:
[
mathbf{t}^{alpha_1 cup alpha_2}_{beta_1cupbeta_2} = 0 quad тогда и только тогда, когда quad
(альфа_1 чашка альфа_2) кап (бета_1чашкабета_2) не = пустойнабор
]
Например:
[
begin{align*}
& mathbf{t}^{12}_{34},mathbf{t}^5_6 = mathbf{t}^{125}_{346} && text{Простая комбинация} \
& mathbf{t}^{12}_{34} ,mathbf{t}^{4} = mathbf{t}^{12{color{red}4}}_{3{color{red}4}} = 0 && text{Исчезает, потому что 4 есть в обоих множествах}
end{align*}
]
Исчезающее произведение означает, что два t-объекта не имеют общих состояний; следовательно, их пересечение пусто.
Эти правила завершают наше построение. Мы определили разреженное представление логики и алгебры для манипулирования объектами. Это все необходимые нам теоретические инструменты. Мы готовы собрать их в практический алгоритм.
Собираем всё вместе: вывод с помощью алгебры состояний
Двигатель готов, пора его запускать! В основе идеи лежит простая идея: чтобы найти множество допустимых состояний, нужно перемножить все векторы состояний, соответствующие предпосылкам и свидетельствам.
Если у нас есть две предпосылки, представленные векторами состояний ((mathbf{t}_{(1)} + mathbf{t}_{(2)})) и ((mathbf{t}_{(3)} + mathbf{t}_{(4)})), множество состояний, в которых оба условия истинны, является их произведением:
[
left(mathbf{t}_{(1)} + mathbf{t}_{(2)}right),left(mathbf{t}_{(3)} + mathbf{t}_{(4)}right) =
mathbf{t}_{(1)},mathbf{t}_{(3)} +
mathbf{t}_{(1)},mathbf{t}_{(4)} +
mathbf{t}_{(2)},mathbf{t}_{(3)} +
mathbf{t}_{(2)},mathbf{t}_{(4)}
]
Этот пример можно легко обобщить на любое произвольное число посылок и t-объектов.
Алгоритм вывода прост:
- Разложить : преобразовать каждую предпосылку в ее векторное представление состояния (сумму t-объектов).
- Упростить : использовать атомарное сокращение для каждого вектора состояния, чтобы сделать его максимально компактным.
- Умножение : перемножьте векторы состояний всех предпосылок. Результатом будет единый вектор состояний, представляющий все состояния, соответствующие вашим предпосылкам.
- Сократите еще раз : конечный продукт может содержать сокращаемые члены, поэтому упростите его еще раз.
Пример: доказательство транзитивности алгебраическим способом
Давайте вернёмся к нашему классическому примеру транзитивности импликации: если (f_1 = (x_1to x_2)) и (f_2 = (x_2to x_3)) истинны, докажите, что (f_3=(x_1to x_3)) также должно быть истинным. Сначала запишем упрощённые векторы состояний для наших посылок следующим образом:
[
begin{align*}
& f_1 quad sim quad mathbf{t}_1 + mathbf{t}^{12} \
& f_2 quad sim quad mathbf{t}_2 + mathbf{t}^{23}
end{align*}
]
Чтобы доказать заключение, можно использовать доказательство от противного. Давайте спросим: существует ли ситуация, в которой наши предпосылки истинны, но наше заключение (f_3) ложно?
Состояния, которые делают недействительным (f_3 = (x_1 to x_3)), — это те, в которых (x_1) истинно (1), а (x_3) ложно (0). Это соответствует одному t-объекту: (mathbf{t}^1_3).
Теперь давайте посмотрим, может ли этот «аннулирующий» вектор состояния сосуществовать с нашими предпосылками, перемножив все между собой:
[
begin{gather*}
(text{Предпосылка 1}) times (text{Предпосылка 2}) times (text{Недействительный вектор состояния})\
(mathbf{t}_1 + mathbf{t}^{12}),(mathbf{t}_2 + mathbf{t}^{23}), mathbf{t}^1_3
end{gather*}
]
Сначала мы умножаем на аннулирующий t-объект, так как это наиболее ограничительный термин:
[
(mathbf{t}_1 mathbf{t}^1_3 + mathbf{t}^{12} mathbf{t}^1_3),(mathbf{t}_2 + mathbf{t}^{23}) = (mathbf{t}^{{color{red}1}}_{{color{red}1}3} + mathbf{t}^{12}_3),(mathbf{t}_2 + mathbf{t}^{23})
]
Первый член, (mathbf{t}^{{color{red}1}}_{{color{red}1}3}), исчезает из-за противоречия. Итак, остаётся:
[
mathbf{t}^{12}_3,(mathbf{t}_2 + mathbf{t}^{23}) =
mathbf{t}^{12}_3 mathbf{t}_2 + mathbf{t}^{12}_3 mathbf{t}^{23} =
mathbf{t}^{1{color{red}2}}_{{color{red}2}3} + mathbf{t}^{12{color{red}3}}_{{color{red}3}} =
0 + 0 = 0
]
Пересечение пусто. Это доказывает, что не существует возможного состояния, в котором (f_1) и (f_2) истинны, но (f_3) ложно. Следовательно, (f_3) должно следовать из посылок.
Доказательство от противного — не единственный способ решения этой задачи. Более подробный анализ можно найти в статье «Государственная алгебра» [1].
От логических головоломок до обнаружения мошенничества
Речь идёт не только о логических головоломках. В нашем мире очень многое подчиняется правилам и логике! Например, представьте себе систему обнаружения мошенничества, основанную на правилах.
Ваша база знаний — это набор правил, таких как
ЕСЛИ местоположение карты находится за рубежом И сумма транзакции > 1000 долларов США, ТО риск высокий
Всю базу знаний можно скомпилировать в один большой вектор состояний.
Итак, транзакция происходит. Вот ваше доказательство:
местоположение_карты = за рубежом, сумма_транзакции > 1000 долларов США, пользователь_вход_в_систему = false
Это доказательство представляет собой единый t-объект, присваивающий 1 наблюдаемым фактам, которые являются истинными, и 0 — фактам, которые являются ложными, оставляя все ненаблюдаемые факты в качестве подстановочных знаков.
Чтобы принять решение, вы просто умножаете:
[
text{Вектор базы знаний}times text{Доказательство T-объект}
]
Результирующий вектор состояния мгновенно определяет значение целевой переменной (например, риска) с учётом имеющихся данных. Никакой запутанной цепочки операторов «если-то-иначе» не потребовалось.
Масштабирование: стратегии оптимизации
Как и в случае с механическими двигателями, существует множество способов сделать наш двигатель более эффективным.
Давайте посмотрим правде в глаза: задачи логического вывода вычислительно сложны, а это значит, что в худшем случае время выполнения неполиномиально. Проще говоря, независимо от компактности представления и интеллекта алгоритма, в худшем случае время выполнения будет чрезвычайно долгим. Настолько долгим, что, скорее всего, вам придётся остановить вычисление до получения результата.
Причина отличной работы SAT-решателей заключается не в том, что они меняют реальность. А в том, что большинство реальных задач не являются наихудшими сценариями. Время выполнения «средней» задачи будет чрезвычайно чувствительно к эвристическим оптимизациям, используемым вашим алгоритмом для вычислений.
Таким образом, эвристика оптимизации может стать одним из важнейших компонентов движка для достижения значимой масштабируемости. Здесь мы лишь намекаем на возможные области, где можно рассмотреть возможность оптимизации.
Обратите внимание, что при умножении большого количества векторов состояний число промежуточных t-объектов может значительно возрасти, прежде чем в конечном итоге сократиться, но мы можем сделать следующее, чтобы обеспечить бесперебойную работу двигателя:
- Постоянное сокращение : после каждого умножения применяется алгоритм сокращения к полученному вектору состояния. Это позволяет сохранить компактность промежуточных результатов.
- Эвристическое упорядочение : порядок умножения имеет значение. Часто лучше сначала умножить меньшие или более ограничивающие векторы состояний, так как это может привести к преждевременному исчезновению большего количества t-объектов, сокращая вычисление.
Заключение
Мы провели вас через путешествие, чтобы узнать, как пропозициональная логика может быть воплощена в формализме векторов состояния, позволяя использовать базовую алгебру для выполнения логического вывода. Элегантность этого подхода заключается в его простоте и эффективности.
Вывод ни в коем случае не требует вычисления гигантских таблиц истинности. База знаний представлена в виде набора разреженных матриц (вектора состояний), а логический вывод сводится к набору алгебраических действий, которые можно реализовать за несколько простых шагов.
Хотя этот алгоритм не претендует на конкуренцию с передовыми решателями SAT и алгоритмами формальной верификации, он предлагает красивый и интуитивно понятный способ представления логики в максимально компактной форме. Это мощный инструмент для создания лёгких механизмов правил и отличная ментальная модель для размышлений о логическом выводе.
Попробуйте сами
Лучший способ понять эту систему — использовать её. Мы упаковали весь алгоритм в открытую библиотеку Python vector-logic. Её можно установить прямо из PyPI:
pip install vector-logic
Полный исходный код вместе с дополнительными примерами и документацией доступен на
GitHub
Мы призываем вас изучить репозиторий, попробовать его на практике для решения собственных логических задач и внести свой вклад.
Если вам интересно глубже изучить математическую теорию, ознакомьтесь с оригинальной статьей [1]. В ней рассматриваются некоторые темы, которые мы не смогли включить в это практическое руководство, такие как каноническая редукция, ортогонализация и многие другие. В ней также предлагается абстрактное алгебраическое представление пропозициональной логики, основанное на формализме t-объектов.
Мы приветствуем любые комментарии и вопросы.
Кто мы
- Дмитрий Лесник
- Тобиас Шефер
Ссылки
[1] Дмитрий Лесник и Тобиас Шефер, «Алгебра состояний для пропозициональной логики», препринт arXiv arXiv:2509.10326, 2025. Доступно по адресу: https://arxiv.org/abs/2509.10326
Источник: towardsdatascience.com
