A - квантор всеобщности;
E - квантор существования;
~ - отрицание;
& - конъюнкция;
V - дизъюнкция;
-> - импликация.
Допускаются только однобуквенные переменные, предикаты и функциональные символы.
Переменные обозначаются строчной буквой, за исключением букв f, g, h, предикаты - заглавной буквой, за исключением букв V, A, E. Для функциональных символов зарезервированы строчные буквы f, g, h.
После квантора всегда идет переменная, к которой он относится.
Пример формулы:
Ax (P(x) V Ey R(x, y)) -> (Ex ~P(x) & AxEzR(x, f(z)))
Парсинг формулы производится с помощью функции str_to_formula(formula_str), которая принимает в качестве аргумента строку и возвращает объект Formula, который можно приводить обратно к строке.
Функция semantic_tableaux_method(formula, output) проивзодит проверку общезначимости формулы методом семантических таблиц.
Принимает первым аргументом объект типа Formula, вторым аргументом - output - переменную булевого типа, обозначающую необходимость печатати в поток стандартного вывода процесс вывода семантической таблицы.
ВНИМАНИЕ!!!
semantic_tableaux_method не поддерживает проверку формул, которые содержат функциональные символы.
Если формула не является общезначимой, функция может работать бесконечно, либо выдавать ошибку.
Функция resolution_method(formula, output) проивзодит проверку общезначимости формулы методом резолюций.
Принимает первым аргументом объект типа Formula, вторым аргументом - output - переменную булевого типа, обозначающую необходимость печатати в поток стандартного вывода процесс преобразования формулы к множеству дизъюнктов и вывода пустого дизъюнкта.
ВНИМАНИЕ!!!
Если формула не является общезначимой, функция может работать бесконечно, либо выдавать ошибку.