Математическая логика на Python 25

Объявления

• Дэдлайн по 1 домашнему заданию - 31.01.25.
• Добавили гугл-класс https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2
• Добавлено ДЗ №2. Дэдлайн - 07.02.25
• Добавлено ДЗ №3. Дэдлайн - 14.02.25
• Теперь все сдаем через github
• Добавлено ДЗ №4. Дэдлайн - 28.02.25
• Добавлено ДЗ №5 Дэдлайн - 14.03.25
• Добавлено ДЗ №6 Дэдлайн - 28.03.25
• Добавлено ДЗ №7 Дэдлайн - 25.04.25
• Добавлено ДЗ №8 Дэдлайн - 16.05.25
• Добавлено ДЗ №9 Дэдлайн - 06.06.25
• Добавлено ДЗ №10 Дэдлайн - 19.06.25

Введение

Этот курс -- попытка представить математическую логику через призму программирования на Python. Такой подход, позваляет студентам использовать интуицию и опыт программированя для изучения логики и, будем надеятся, сделает логику более доступной и наглядной. Практическая работа с кодом позволяет глубже понять концепции математической логики и увидеть работу этих концепций в реальных программах.

Описание курса

Курс включает пропозициональную логику и логику первого порядка. При этом планируется логику планируется изложить на уровне полноценного курса по математической логики со всеми важными теоремами и доказательствами. В качестве литературы можно использовать Н. К. Верещагин, А. Шень. Часть 2. Языки и исчисления. 5-е изд., М.: МЦНМО, 2017.

С другой стороны будет уделено много внимание тому как реализовать все формальные конструкции на языке Python и тут мы будем в основном следовать материалам на сайте https://www.logicthrupython.org/ Вместо решения обычных задач на семинарах мы будем писать программы, которые реализуют используемые в курсе конструкции. Имеются шаблоны программ, в которых недописаны некоторые куски кода, которые студенты должны дописать, чтобы в результате получилась работающая программа. В шаблонах имеются тесты, которые позволяют проверить работоспособность.

Формула оценки

В формуле участвуют: ДЗ -- доля пройденных тестов в заданиях на Python умноженная на 10. Колл -- оценка за коллоквиум, который пройдет после 3 модуля во время сессии (по 10 бальной шкале). Экз -- оценка за экзамен (по 10 бальной шкале)

Автомат будет выставлятся при условии, что MIN(ДЗ, Колл) >= 8. В этом случае итоговая оценка будет равна (2*ДЗ+Колл)/3, с округлением к ближайшему целому числу.

Итоговая оценка = 0.5 ДЗ + 0.25 Колл + 0.25 Экз

Домашние задания

Домашнее задание №1 (дэдлайн 31.01.25)

В этом задании вам надо будет внести изменения в файл propositions/syntax.py

Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2

Задание 1.1 (Task 1.1) В файле мето отмечено следующим комментарием: # Task 1.1

Реализуйте недостающий код для метода __repr__() класса Formula, который возвращает строку, представляющую формулу (в синтаксисе, определённом в Определении 1.1).

Обратите внимание, что в Python строка, возвращаемая методом formula.__repr__(), также возвращается вызовом str(formula). Таким образом, решив эту задачу, вы также реализуете функциональность метода str() для данного класса.

Задание 1.2 (Task 1.2) Реализуйте недостающий код для метода variables() класса Formula, который возвращает множество (set) имен переменных, присутствующие в формуле. Напомним, что имя переменной — это лист дерева, метка которого является буквой от «p» до «z», за которой следуют цифры.

Задание 1.3 (Task 1.3)

Реализуйте недостающий код для метода operators() класса Formula, который возвращает все операторы, присутствующие в формуле. Операторами в этом задании являются не только все унарные и бинарные операторы, но и константы T и F.

Задание 1.4 (Task 1.4)

Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, и возвращает формулу (объект типа Formula), созданное из префикса строки, а также строку, содержащую непроанализированный остаток строки (которая может быть пустой, если вся строка образует формулу). Обратите внимание, что формула это очень строгое формальное понятие, обратите внимание на скобки.

Задание 1.5 (Task 1.5)

Реализуйте недостающий код для статичного метода is_formula(string) класса Formula, который проверяет, представляет ли заданная строка корректную формулу.

Подсказка: используйте метод _parse_prefix().

Задание 1.6 (Task 1.6)

Реализуйте недостающий код для статичного метода parse(string) класса Formula, который разбирает строковое представление формулы. (Можно предположить, что входная строка корректна, то есть удовлетворяет предусловию Formula.is_formula(string), в коде уже есть соответствующий assert)

Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter01.py

Домашнее задание №2 (дэдлайн 07.02.25)

В этом задании вам надо будет внести изменения в файл propositions/semantics.py

Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2

Задание 2.1 (Task 2.1)

Реализуйте недостающий код для функции evaluate(formula, model), которая возвращает истинностное значение данной формулы (formula) в данной модели (model).

Задание 2.2 (Task 2.2)

Реализуйте недостающий код для функции all_models(variables), которая возвращает список всех возможных моделей над заданными именами переменных. Обратите внимание, что модели должны выводиться в лексикографическом порядка, считая, что F меньше T.

Задание 2.3 (Task 2.3)

Реализуйте недостающий код для функции truth_values(formula, models), которая возвращает список истинностных значений данной формулы (formula) в данных моделях (models).

Задание 2.4 (Task 2.4)

Реализуйте недостающий код для функции print_truth_table(formula), которая выводит таблицу истинности данной формулы (переменные должны быть отсортированы лексикографически, и строки в таблице тоже должны идти в лексикографическом порядке).

Задание 2.5 (Task 2.5a, Task 2.5b, Task 2.5c)

Реализуйте недостающий код для функций is_tautology(formula), is_contradiction(formula) и is_satisfiable(formula), которые соответственно определяют, является ли данная формула тавтологией, тождественно ложной или выполнимой.

Задание 2.6 (Task 2.6)

Реализуйте недостающий код для функции _synthesize_for_model(model), которая возвращает формулу высказываний в виде элементарной конъюнкции, принимающую значение True на данной модели и False на всех остальных моделях с теми же именами переменных.

Задание 2.7 (Task 2.7)

(Программное доказательство теоремы о ДНФ) Реализуйте недостающий код для функции synthesize(variables, values), которая строит формулу высказываний в дизъюнктивной нормальной форме (ДНФ) по заданному описанию её таблицы истинности.

Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter02.py

Домашнее задание №3 (дэдлайн 14.02.25)

В этом задании вам надо будет внести изменения в файлы: propositions/semantics.py , propositions/syntax.py и propositions/operators.py

Загрузить можно в гугл классе.

Задание 1 (Task 3.1)

Расширьте класс Formula из главы 1, добавив поддержку четырех новых бинарных операторов: +, <->, -&, -|.

• Измените функцию is_binary() в файле propositions/syntax.py. (По сути надо закоментить старый функционал и раскоментить строчку с новым функционалом)
• Внесите необходимые изменения в метод _parse_prefix() класса Formula.
• Проверьте, что все методы (как экземпляра, так и статические), реализованные в этом классе в главе 1, теперь работают корректно для всех семи бинарных операторов (старых и новых). (Для этого достаточно запустить тест для 3 главы и если будут ошибки - исправить их)
• Если код написан правильно, дополнительных изменений, кроме указанных выше, не потребуется.

Задание 2 (Task 3.2)

Расширьте функцию evaluate() из главы 2, добавив поддержку четырех новых операторов.

Проверьте, что функции truth_values(), print_truth_table(), is_tautology(), is_contradiction() и is_satisfiable() автоматически приобретают поддержку этих операторов благодаря изменениям в evaluate().

Задание 3 (Task 3.3)

Реализуйте недостающий код для метода substitute_variables(substitution_map) класса Formula.

Метод принимает на вход словарь, сопоставляющий некоторые переменные с формулами, и возвращает новую формулу, полученную путем замены переменных на их значения (формулы) из словаря.

Задание 4 (Task 3.4)

Реализуйте недостающий код для метода substitute_operators(substitution_map) класса Formula.

• Метод принимает словарь, где ключи — операторы, а значения — формулы, использующие только переменные p и q.
• Переменная p служит заместителем первого операнда (если оператор унарный или бинарный), q — второго (если оператор бинарный).
• Метод возвращает новую формулу, в которой каждый оператор из словаря заменен соответствующей формулой, при этом p и q подставляются вместо исходных операндов.
• Если оператор — константа (T или F), то он просто заменяется на соответствующую формулу без подстановки переменных.

Задание 5 (Task 3.5)

Реализуйте недостающий код для функции to_not_and_or(formula), которая возвращает формулу, эквивалентную данной (то есть имеющую ту же таблицу истинности), но использующую только операторы not, and и or.

Задание 6 (Task 3.6a, Task 3.6b, Task 3.6c, Task 3.6d)

Реализуйте недостающий код для следующих четырех функций:

• to_not_and(formula)
• to_nand(formula)
• to_implies_not(formula)
• to_implies_false(formula)

Каждая из них должна возвращать формулу, эквивалентную данной, но использующую только операторы, указанные в названии функции.

Домашнее задание №4 (дэдлайн 28.02.25)

В этот раз мы настроим систему загрузки решения в classroom.github.com Подробная инструкция появится чуть позже.

Задание 1 (Task 4.1) Файл: proofs.py

Реализуйте недостающий код для метода variables() класса InferenceRule, который возвращает множество имен переменных, встречающихся в предположениях и/или в заключении правила.

---

Задание 2 (Task 4.2) Файл: semantics.py

Реализуйте недостающий код для функции evaluate_inference(rule, model), которая возвращает True, если данное правило вывода выполняется в заданной модели, и False в противном случае.

Правило считается выполненным, если не существует модели, в которой все предположения истинны, а заключение ложно.

---

Задание 3 (Task 4.3) Файл: semantics.py

Реализуйте недостающий код для функции is_sound_inference(rule), которая проверяет, является ли данное правило вывода корректным, то есть сохраняет ли оно истинность формул в любой модели.

---

Задание 4 (Task 4.4) Файл: proofs.py

Реализуйте недостающий код для метода specialize(specialization_map) класса InferenceRule, который возвращает частный случай данного правила вывода согласно заданной подстановке.

Подсказка: Используйте метод substitute_variables() класса Formula, реализованный в ДЗ 3.

---

Задание 5 (Task 4.5) Файл: proofs.py

В этой задаче требуется определить, является ли одно правило вывода частным случаем другого, и, если это так, найти соответствующую карту специализации.

a. Реализуйте недостающий код статичного метода _merge_specialization_maps(map1, map2) класса InferenceRule. Метод должен проверить совместимость двух карт специализации (т.е. проверить, чтобы одно и то же имя переменной не отображалось в разные формулы) и, если карты совместимы, вернуть их объединение, иначе None.

b. Реализуйте недостающий код статичного метода _formula_specialization_map(general, specialization) класса InferenceRule. Метод должен вернуть словарь подходящей замены, если вторая формула является частным случаем первой, иначе None.

Подсказка: Используйте метод _merge_specialization_maps().

c. Реализуйте недостающий код метода specialization_map(specialization) класса InferenceRule, который возвращает словать замены, если правило-аргумент является частным случаем текущего (self), иначе None.

Важно: Порядок посылок должен сохраняться.

---

Задание 6 (Task 4.6) Файл: proofs.py

Проверьте корректность данного доказательства, т.е. убедитесь, что каждая строка является либо допущением, либо корректным выводом из предыдущих строк согласно допустимым правилам вывода.

a. Реализуйте недостающий код метода rule_for_line(line_number) класса Proof, который возвращает правило вывода для указанной строки.

Пояснение: Например, если в строке стоит формула A, и в списке формул посылок (порядок важен!) указаны формулы B1, ..., Bn, то вернуть нужно правило с посылками B1, ..., Bn и заключением A.

b. Реализуйте недостающий код метода is_line_valid(line_number) класса Proof, который проверяет корректность указанной строки.

Подсказка: Используйте метод rule_for_line().

c. Реализуйте недостающий код метода is_valid() класса Proof, который возвращает True, если доказательство корректно, иначе False.

---

Правило вывода Г/A называется допустимым, если A логически следует из Г.

Задание 7 (Task 4.7) Файл: some_proofs.py

Докажите допустимость правила вывода с посылкой (p&q) и заключением (q&p) с помощью следующих правил:

• Правило 1: Предположения: x, y; Заключение: (x&y)
• Правило 2: Предположение: (x&y); Заключение: y
• Правило 3: Предположение: (x&y); Заключение: x

Вывод, доказывающий допустимость, должен быть возвращен функцией prove_and_commutativity().

---

Задание 8 (Task 4.8) Файл: some_proofs.py

Правила упомянутые в этом задании правила вывода есть в файле axiomatic_systems.py. Их можно оттуда импортировать.

Докажите допустимость правила вывода с заключением (p->p) без посылок, используя правила MP, I1 и D.

Вывод, доказывающий допустимость, должен быть возвращен функцией prove_I0().

---

Задание 9 (Task 4.9) Файл: soundness.py

Реализуйте функцию rule_nonsoundness_from_specialization_nonsoundness(general, specialization, model), которая для заданного правила вывода, его частного случая и модели, являющейся контрпримером для частному случаю, возвращает модель, являющуюся контрпримером для исходного правила.

---

Задание 10 (Task 4.10) Файл: soundness.py

Реализуйте функцию nonsound_rule_of_nonsound_proof(proof, model), которая для корректного вывода и модели, являющейся контрпримером для заключения доказательства, возвращает некорректное правило вывода, использованное в доказательстве, а также модель-контрпример для этого правила.

---

Каждое задание проверяйте на корректность с помощью тестов в файле test_chapter04.py.

Домашнее задание №5 (дэдлайн 14.03.25)

Задание 5.1 (Task 5.1) file:propositions/proofs.py

Реализуйте недостающий код для функции prove_specialization(proof, specialization), которая принимает корректное доказательство некоторого правила вывода и возвращает дедуктивное доказательство (вывод) частного случая этого правила, используя то же множество правил вывода.

Подсказка: Используйте метод specialization_map() класса InferenceRule для получения карты замены, которое надо сделать в правиле, доказываемое в proof, чтобы получить правило specialization.

Задание 5.2 (Task 5.2) file:propositions/proofs.py

Реализуйте недостающий код для функции inline_proof(main_proof, lemma_proof), которая принимает доказательство (вывод) main_proof некоторого правила вывода с использованием множества правил R и дедуктивное доказательство lemma_proof одного из правил λ из R (леммы) с использованием множества правил R' (где λ не лежит в R') и возвращает доказательство правила вывода, доказанного в main_proof, но с использованием множества правил R \ {λ} ∪ R'.

а. Сначала реализуйте функцию _inline_proof_once(main_proof, line_number, lemma_proof), которая заменяет один экземпляр использования данной леммы в доказательстве.

б. Затем реализуйте inline_proof(main_proof, lemma_proof), вызывая _inline_proof_once() до тех пор, пока все вхождения данной леммы не будут удалены.

Задание 5.3 (Task 5.3) file:propositions/deduction.py

а. Реализуйте недостающий код для функции prove_corollary(antecedent_proof, consequent, conditional), которая принимает доказательство некоторой формулы φ (посылки) из некоторых предположений, желаемое заключение ψ и правило вывода conditional, для которого ‘(φ → ψ)’ является частным случаем, и возвращает доказательство ψ из тех же предположений, используя те же правила вывода, а также MP и conditional.

б. Реализуйте более сложный вариант функции combine_proofs(antecedent1_proof, antecedent2_proof, consequent, double_conditional), которая принимает два доказательства формул φ1 и φ2 (посылок), выведенных из одних и тех же предположений с использованием одних и тех же правил вывода, а также желаемое заключение ψ и правило вывода double_conditional, для которого ‘(φ1 → (φ2 → ψ))’ является с

Задание 5.4 (Task 5.4) file:propositions/deduction.py

Реализуйте недостающий код для функции remove_assumption(proof), которая принимает доказательство (вывод) некоторого заключения ψ из непустого списка посылок с использованием правил вывода, которые, кроме MP, не имеют посылок, и возвращает доказательство ‘(φ → ψ)’, где φ — последняя посылка правила (тут важно, что посылки - это не множество, а упорядоченный список и последняя посылка - это формула, стоящая в конце этого списка), которое доказывает proof, из тех же посылок, за исключением φ, с использованием того же множества правил, а также MP, I0, I1 и D.

Задание 5.5 (Task 5.5) file:propositions/some_proofs.py

Докажите следующее правило вывода:

• Посылки: ‘(p → q)’, ‘(q → r)’
• Заключение: ‘(p → r)’
• Множество правил: MP, I0, I1, D

Доказательство должно быть реализовано в функции prove_hypothetical_syllogism() в файле propositions/some_proofs.py.

Подсказка: Используйте теорему о дедукции, реализованную в Task 5.4.

Задание 5.6 (Task 5.6) file:propositions/deduction.py

Реализуйте недостающий код для функции proof_from_opposites(proof_of_affirmation, proof_of_negation, conclusion), которая принимает доказательство формулы φ и доказательство её отрицания ‘~φ’, оба с использованием одних и тех же правил вывода и из одних и тех же посылок, а также произвольное заключение (формулу) conclusion. Функция должна вернуть доказательство формулы conclusion из тех же посылок, используя те же правила вывода, что в доказательствах, а также MP и I2.

Подсказка: Функция combine_proofs(), реализованная в Task 5.3, может упростить применение аксиомы I2.

Задание 5.7 (Task 5.7) file:propositions/deduction.py

Реализуйте недостающий код для функции prove_by_way_of_contradiction(proof), которая принимает доказательство ‘~(p → p)’ из некоторых предположений, а также из отрицания ‘~φ’ некоторой формулы, и возвращает доказательство φ из этих предположений (без ‘~φ’) с использованием тех же правил вывода, а также MP, I0, I1, D и N.

Подсказка: Используйте теорему о дедукции (remove_assumption(proof)) и затем аксиому N.

Домашнее задание №6 (дэдлайн 28.03.25)

Задание 6.1 (Task 6.1) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции formulas_capturing_model(model), которая возвращает список формул (переменных или их отрицаний), описывающий данную модель (то, что на лекции обозначалось Г_М). Обратите внимание, что список должен быть упорядочен в лексикографическом порядке.

b. Реализуйте недостающий код для функции prove_in_model(formula, model), которая принимает пропозициональную формулу (содержащую только операторы '->' и '~') и модель, и возвращает либо вывод (proof) самой формулы (если она истинна в данной модели), либо вывод её отрицания (если формула ложна в данной модели) из множества Г_М в стандартной системе правил (AXIOMATIC_SYSTEM из axiomatic_systems.py).

Задание 6.2 (Task 6.2) (file: propositions/tautology.py)

Реализуйте недостающий код для функции reduce_assumption(proof_from_affirmation, proof_from_negation). Эта функция принимает два доказательства, оба доказывающих одно и то же заключение, используя одни и те же правила вывода, но из разных списков посылок. Списоки посылок должны быть почти одинаковые, за исключением последней формулы, т.е. последняя формула в списке посылок вывода proof_from_negation должна являться отрицанием последней формулы в списке посылок вывода proof_from_affirmation.

Функция должна вернуть вывод того же заключения, но уже из списка посылок, которые являются общими для обоих доказательств (то есть всех формул, кроме последних в списках посылок каждого вывода). Вывод должен использовать правила вывода, как в исходных выводах, а также также включать правила MP, I0, I1, D и R (их можно импортировать из модуля axiomatic_systems.py).

Подсказка: Используйте теорему о дедукции и аксиому R.

Задание 6.3 (Task 6.3) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции prove_tautology(tautology, model), которая возвращает доказательство данной тавтологии в рамках нашей стандартной аксиоматической системы, используя множество посылок, описывающее данную модель (Г_М). Если модель построена на пустом множестве посылок (по умолчанию), возвращаемое доказательство должно доказывать тавтологию без предположений.

Рекомендации:

Если модель содержит все переменные, входящие в тавтологию, просто постройте доказательство с помощью prove_in_model(tautology, model).

В противном случае рекурсивно вызовите prove_tautology() с моделями, в которых также задано значение для следующей неуказанной переменной, а затем используйте функцию reduce_assumption().

b. Реализуйте недостающий код для функции proof_or_counterexample(formula), которая либо возвращает доказательство данной формулы без посылок в рамках нашей аксиоматической системы (если эта формула является тавтологией), либо возвращает модель, в которой данная формула не выполняется (если формула не является тавтологией).

Задание 6.4 (Task 6.4) (file: propositions/tautology.py)

a. Реализуйте недостающий код для функции encode_as_formula(rule), которая возвращает формулу, "кодирующую" данное правило вывода (как кодировать было на лекции). Формула единственным образом задается по правилу, учитывая, что посылки в rule задаются упорядоченным списком [A1, A2, ..., An]. Для этого списка посылок и заключения B "кодирующая" формула выглядит так: (A1->(A2->(...(An->B)...)))

b. Реализуйте недостающий код для функции prove_sound_rule(rule), которая принимает корректное правило вывода и возвращает его доказательство в нашей стандартной аксиоматической системе.

Задание 6.5 (Task 6.5) (file: propositions/tautology.py)

Реализуйте недостающий код для функции model_or_inconsistency(formulas), которая возвращает либо модель, в которой выполняются данные формулы (если такая модель существует), либо доказательство ~(p → p) в нашей стандартной аксиоматической системе из данных формул в качестве посылок (если такая модель не существует).

Подсказка:

Если модели для данных формул не существует, то что можно сказать о правиле вывода, где посылками являются данные формулы, а заключением – ~(p -> p)?

Является ли оно корректным? Почему?

Как можно использовать решение задания 6.4 для завершения текущего задания?

Постарайтесь осознать, как код который вы пишите повторяет доказательства, которые были на лекциях.

Домашнее задание №7 (дэдлайн 25.04.25)

Задание 7.1 (Task 7.1) (file: predicates/syntax.py)

Реализуйте недостающий код для метода __repr__() класса Term, который возвращает строку, представляющую терм (в соответствии с определением на лекции, в английской книге Definition 7.1).

Задание 7.2 (Task 7.2) (file: predicates/syntax.py)

Реализуйте недостающий код для метода __repr__() класса Formula, который возвращает строку, представляющую формулу (в соотвествии с определением формулы, сделанном на лекции, в английском учебнике это Definition 7.2).

Задание 7.3 (Task 7.3) (file: predicates/syntax.py)

a. Реализуйте недостающий код для статического метода _parse_prefix(string) класса Term, который принимает строку, содержащую префикс, представляющий терм, и возвращает объект типа Term и оставшуюся неразобранную часть строки.

b. Реализуйте недостающий код для статического метода parse(string) класса Term, который разбирает строковое представление терма. Можно считать, что входная строка представляет корректный терм.

Задание 7.4 (Task 7.4) (file: predicates/syntax.py)

a. Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, содержащую префикс, представляющий формулу, и возвращает объект типа Formula и оставшуюся неразобранную часть строки.

b. Реализуйте недостающий код для статического метода parse(string) класса Formula, который разбирает строковое представление формулы. Можно считать, что входная строка представляет корректную формулу.

Задание 7.5 (Task 7.5) (file: predicates/syntax.py)

Реализуйте недостающий код для методов constants(), variables() и functions() класса Term, которые возвращают, соответственно: все имена констант, все имена переменных и все имена функций (с их арностями), встречающиеся в терме. Можно считать, что любая функция всегда вызывается с одной и той же арностью.

Задание 7.6 (Task 7.6) (file: predicates/syntax.py)

Реализуйте недостающий код для методов constants(), variables(), free_variables(), functions() и relations() класса Formula, которые возвращают, соответственно: все имена констант, все имена переменных, все свободные переменные, все имена функций (с их арностями) и все имена отношений (с их арностями), встречающиеся в формуле. Можно считать, что любая функция или отношение всегда вызываются с одной и той же арностью.

Задание 7.7 (Task 7.7) (file: predicates/semantics.py)

Реализуйте недостающий код для метода evaluate_term(term, assignment) класса Model, который возвращает значение терма при заданном назначении переменных (значение терма должно принадлежать носителю модели).

Задание 7.8 (Task 7.8) (file: predicates/semantics.py)

Реализуйте недостающий код для метода evaluate_formula(formula, assignment) класса Model, который возвращает истинностное значение формулы при заданном назначении её свободных переменных.

Задание 7.9 (Task 7.9) (file: predicates/semantics.py)

Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.

Домашнее задание №8 (дэдлайн 16.05.25)

Задание 8.1 (Task 8.1) (file: predicates/functions.py) Реализуйте недостающий код для функции replace_functions_with_relations_in_model(model), которая возвращает бесфункциональный аналог данной модели. Каждому имени функции должено соответствовать имя предиката в новой модели, причем имя должно быть каноническое (см. лекции, или книжку).

Задание 8.2 (Task 8.2) (file: predicates/functions.py) Реализуйте недостающий код для функции replace_relations_with_functions_in_model(model, original_functions), которая возвращает модель с интерпретациями для заданных имён функций (из множества original_functions и только для них), чей бесфункциональный аналог совпадает с моделью model.

Подсказка: Функция должна возвращать None, если для какого-то имени функции не существует соответствующего отношения в модели, удовлетворяющего условию функциональности и тотальности (для каждого набора аргументов существует ровно один результат).

Задание 8.3 (Task 8.3) (file: predicates/functions.py) Реализуйте недостающий код для функции _compile_term(term), которая принимает терм с вызовом функции (возможно, с вложенными вызовами) и возвращает «шаги», разбивающие терм на формулы вида y=f(x1,…,xn), где y — новое имя переменной, f — имя функции, а xi — константы или переменные. Новые имена переменных должны генерироваться через next(fresh_variable_name_generator).

Примечание: Можно считать, что сгенерированные имена переменных не встречаются в исходном терме.

Задание 8.4 (Task 8.4) (file: predicates/functions.py) Реализуйте недостающий код для функции replace_functions_with_relations_in_formula(formula), которая возвращает функциональный аналог формулы без функций.

Подсказка: Используйте рекурсию для формул с кванторами и булевыми операторами.

Задание 8.5 (Task 8.5) (file: predicates/functions.py) Реализуйте недостающий код для функции replace_functions_with_relations_in_formulas(formulas), которая возвращает формулу, содержащую:

1. Бесфункциональные аналоги для всех заданных формул.

2. Для каждого имени функции в формулах — формулы, проверяющие, что соответствующее отношение действительно задаёт функцию.

Задание 8.6 (Task 8.6) (file: predicates/functions.py) Реализуйте недостающий код для функции replace_equality_with_SAME_in_formulas(formulas), которая возвращает формулы без равенства, заменяя его на отношение SAME, и добавляет формулы, обеспечивающие его свойства (рефлексивность, симметричность, транзитивность и согласованность с другими предикатами и фукнциями).

Задание 8.7 (Task 8.7) (file: predicates/functions.py) Реализуйте недостающий код для функции add_SAME_as_equality_in_model(model), которая возвращает модель, идентичную исходной, но с добавлением интерпретации отношения SAME, соответствующего равенству.

Задание 8.8 (Task 8.8) (file: predicates/functions.py) Реализуйте недостающий код для функции make_equality_as_SAME_in_model(model), которая возвращает модель без интерпретации SAME, содержащую по одному представителю из каждого класса эквивалентности SAME.

Требование: Для любой модели model и формул new_formulas=replace_equality_with_SAME_in_formulas(formulas) должно выполняться: model является моделью new_formulas тогда и только тогда, когда make_equality_as_SAME_in_model(model) является моделью formulas.

Домашнее задание №9 (дэдлайн 06.06.25)

Задание 9.1 (Task 1) (file: predicates/syntax.py)

Реализуйте недостающий код метода `substitute(substitution_map, forbidden_variables)` класса `Term`. Метод должен возвращать терм, полученный из текущего терма заменой всех вхождений имён переменных и констант, являющихся ключами словаря `substitution_map`, на соответствующие термы-значения из этого словаря.

Если при такой подстановке какой-либо из термов, на который производится замена, содержит переменную из множества `forbidden_variables`, необходимо вызвать исключение `ForbiddenVariableError` (определено в файле `predicates/syntax.py`).

---

Задание 9.2 (Task 2) (file: predicates/syntax.py)

Реализуйте недостающий код метода `substitute(substitution_map, forbidden_variables)` класса `Formula`. Метод должен возвращать формулу, полученную из текущей формулы путём:

– замены всех вхождений имён констант, указанных в `substitution_map`, на соответствующие термы; – замены всех свободных вхождений имён переменных, указанных в `substitution_map`, на соответствующие термы.

Если подставляемый терм содержит переменную из множества `forbidden_variables`, или если переменная в нём становится связанной после подстановки, необходимо вызвать исключение `ForbiddenVariableError`.

Подсказка: используйте рекурсию, дополняя множество `forbidden_variables` переменными, связанными в текущем подвыражении. В базовом случае воспользуйтесь вашим решением из Задания 9.1.

---

Задание 9.3 (Task 3) (file: predicates/syntax.py)

Реализуйте недостающий код статичного метода `_instantiate_helper` класса `Schema`.

Этот рекурсивный метод принимает четыре аргумента:

1. Формулу. 2. Словарь `constants_and_variables_instantiation_map`, сопоставляющий каждому шаблонному имени переменной или константы терм, на который оно должно быть заменено. Имя переменной можно заменить только на терм, являющийся переменной. 3. Словарь `relations_instantiation_map`, сопоставляющий каждому шаблонному предикату (с параметрами или без) формулу, которую следует подставить вместо него. В случае параметризованных шаблонов используется имя константы `'_'` (подчеркиваение). 4. Множество `bound_variables` — имён переменных, которые считаются связанными на внешних уровнях рекурсии.

Метод должен возвращать формулу, полученную из входной путём выполнения всех подстановок.

Метод вызывает исключение `Schema.BoundVariableError`, если: – формула, подставляемая вместо шаблонного предиката, содержит свободную переменную из `bound_variables`; – подстановка приводит к тому, что ранее свободная переменная становится связанной.

Подсказка: реализуйте метод рекурсивно. – Простые базовые случаи: обычное равенство или предикат без параметров — используйте метод `substitute()` класса `Formula`, игнорируя `bound_variables`. – В случае нульарного шаблонного предиката — возвращайте соответствующую формулу (предварительно проверив, что её свободные переменные не пересекаются с `bound_variables`). – В случае унарного шаблонного предиката вида `R(t)` — сначала подставьте `t`, затем «впишите» результат в соответствующую формулу с помощью `Formula.substitute({'_': t0})`. Проверьте, что свободные переменные заменяемой формулы не входят в `bound_variables`.

Рекурсивный обход формулы прост, за исключением случая кванторов `Ax[...]` и `Ex[...]`. Если имя переменной квантора — шаблонное, оно должно быть заменено. В любом случае имя связанной переменной должно быть добавлено в `bound_variables` при рекурсивном вызове.

---

Задание 9.4 (Task 4) (file: predicates/proofs.py)

Реализуйте недостающий код метода `instantiate(instantiation_map)` класса `Schema`. Метод принимает отображение от шаблонов текущей схемы к объектам, которыми их нужно заменить, и возвращает результат подстановки.

Если `instantiation_map` ссылается на имя, не являющееся шаблонным, или нарушает условия из Раздела 9.2.3, метод должен вернуть `None`.

Рекомендация: используйте ваше решение из Задания 9.3, передав в него соответствующие аргументы. Не забудьте обработать исключения, которые может вызывать `_instantiate_helper()`.

---

Задание 9.5 (Task 5) (file: predicates/proofs.py)

Реализуйте недостающий код метода `is_valid(assumptions, lines, line_number)` класса `Proof.AssumptionLine`. Метод должен возвращать `True`, если формула текущей является аксиомой или гипотезой, а именно, является частным случаем одной из схем аксиом или гипотез (посылок) доказательства.

Подсказка: метод принимает три аргумента (`assumptions`, `lines`, `line_number`) для согласованности с методами `is_valid` других строк доказательства. Возможно, вам не понадобятся все три.

---

Задание 9.6 (Task 6) (file: predicates/proofs.py)

Реализуйте недостающий код метода `is_valid(assumptions, lines, line_number)` класса `Proof.MPLine`. Метод должен проверять, корректно ли текущая строка получена с помощью Modus Ponens из двух предыдущих.

Подсказка: структура аргументов та же, что и в предыдущих заданиях.

---

Задание 9.7 (Task 7) (file: predicates/proofs.py)

Реализуйте недостающий код метода `is_valid(assumptions, lines, line_number)` класса `Proof.UGLine`. Метод должен проверять, корректно ли текущая строка получена с помощью правила обобщения (Universal Generalization) из предыдущей строки.

---

Задание 9.8 (Task 8) (file: predicates/syntax.py)

Реализуйте недостающий код метода `propositional_skeleton()` класса `Formula`. Метод должен возвращать пару: пропозициональную формулу (объект `propositions.syntax.Formula`) и словарь, сопоставляющий переменным вида `z8` соответствующие подформулы исходной формулы, которые они заменили.

Рекомендации: – Имена переменных пропозициональной формулы должны быть `z1`, `z2`, …, в порядке первого появления в исходной формуле. – Используйте генератор `fresh_variable_name_generator`, импортированный из `predicates/util.py`, чтобы создавать имена.

---

Задание 9.9 (Task 9) (file: predicates/proofs.py)

Реализуйте недостающий код метода `is_valid(assumptions, lines, line_number)` класса `Proof.TautologyLine`. Метод должен проверять, является ли формула текущей строки действительно тавтологией.

Подсказка: – Используйте решение из Задания 9.8. – Функция `is_propositional_tautology()` уже импортирована из `propositions.semantics`.

---

Задание 9.10 (Task 10) (file: predicates/syntax.py)

Реализуйте недостающий код статического метода `from_propositional_skeleton(skeleton, substitution_map)` класса `Formula`. Метод должен возвращать формулу предикатной логики, которая могла бы быть результатом вызова `propositional_skeleton()` (не накладывая ограничений на имена переменных и порядок).

---

Задание 9.11 (Task 11) (file: predicates/proofs.py)

a. Реализуйте недостающий код функции `_axiom_specialization_map_to_schema_instantiation_map(propositional_specialization_map, substitution_map)`. Функция принимает: – отображение `propositional_specialization_map`, показывающее, как аксиома пропозициональной логики `axiom` специализируется в формулу `specialization`; – отображение `substitution_map`, по которому `specialization` преобразуется в формулу предикатной логики `formula` с помощью `Formula.from_propositional_skeleton`.

Функция должна вернуть отображение для подстановки в схему, эквивалентную `axiom` (например, `I0_SCHEMA` вместо `I0`), которое позволяет получить формулу `formula`.

Подсказка: можно предполагать, что ключи `propositional_specialization_map` — подмножество `{p, q, r}`.

b. Реализуйте недостающий код функции `_prove_from_skeleton_proof(formula, skeleton_proof, substitution_map)`. Функция принимает: – формулу предикатной логики `formula`; – доказательство пропозиционального скелета `skeleton` формулы `formula`; – отображение `substitution_map`, соответствующее скелету.

Функция должна вернуть доказательство `formula` в предикатной логике (в системе `PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS`), содержащее только строки с посылками и MP.

Рекомендации: – Поскольку в `skeleton_proof` нет посылок, каждая строка — либо MP, либо специализация аксиомы. – Для MP используйте те же номера строк. – Для специализации используйте решение пункта (a). – Переводите формулы с помощью метода `from_propositional_skeleton`.

---

Задание 9.12 (Task 12) (file: predicates/proofs.py)

Реализуйте недостающий код функции `prove_tautology(tautology)`. Функция должна доказывать указанную тавтологию предикатной логики с использованием только аксиом схем и правила MP (`PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS`).

Подсказка: – Используйте `prove_propositional_tautology()` (импортирована из `propositions.tautology`). – Затем примените вашу функцию `_prove_from_skeleton_proof`.

Домашнее задание №10 (дэдлайн — 19.06.25)

В этом задании вам предстоит реализовать недостающие методы класса Prover в файле predicates/prover.py, а нескольких заданиях реализовать статичные методы в файле predicates/some_proofs.py, которые выдают доказательства некоторых утверждений. Каждый из пунктов подразумевает добавление в доказательство новых строк, обоснованных допустимыми правилами логики первого порядка с равенством. Следуйте примерам и комментариям в коде.

Задание 10.1 (Task 10.1)

Реализуйте метод add_universal_instantiation(instantiation, line_number, term) (в классе Prover). Метод должен добавлять корректные строки к доказательству (выводу), последняя из которых — формула instantiation, полученная подстановкой терма term вместо свободных вхождений переменной x в формуле из строки line_number, которая должна быть универсальной квантификацией вида Ax[φ(x)].

Обратите внимание, что параметр instantiation может быть передан, как строка. В методе уже реализована конвертация строки в формулу. То же самое верно относительно всех параметров типа Formula и Term в методах класса Prover.

Например, если в строке 17 стоит формула Ay[(Q(y, z) -> R(w, y))], то вызов

prover.add_universal_instantiation('(Q(f(1, w), z) -> R(w, f(1, w)))', 17, 'f(1, w)') 

должен добавить строки, заканчивающиеся формулой (Q(f(1, w), z) -> R(w, f(1, w))).

Задание 10.2 (Task 10.2)

Реализуйте метод add_tautological_implication(implication, line_numbers). Он должен добавлять корректные строки к доказательству, последняя добавленная строка должна содержать формулу implication, являющуюся тавтологическим следствием формул, стоящих в строках, указанных в line_numbers. Формально, если формула B — тавтологическое следствие формул A1, A2, ..., An, то импликация

(A1 & A2 & ... & An) -> B 

является логической тавтологией. Этим можно воспользоваться для вывода.

Подсказка: вспомните задачу №4 в домашнем задании №6, котором реализовался метод prove_sound_inference().

Задание 10.3 (Task 10.3)

Реализуйте метод add_existential_derivation(consequent, line_number1, line_number2). Метод должен добавить строки, последняя из которых — формула consequent. В строке line_number1 должна стоять формула вида Ex[φ(x)], а в строке line_number2 — формула φ(x) -> consequent.

Задание 10.4 (Task 10.4)

Реализуйте функцию prove_lovers() так, чтобы она возвращала корректное доказательство следующего вывода из множества посылок:

Посылки: (1) AxEy[Loves(x, y)] — "каждый любит кого-то"; (2) AxAzAy[(Loves(x, y) -> Loves(z, x))] — "каждый любит тех, кто любит". Заключение: AxAz [Loves(z, x)] — "каждый любит каждого".

Задание 10.5 (Task 10.5)

Реализуйте функцию prove_homework(...) так, чтобы она доказывала следующее: Посылки: (1) ~Ex[Homework(x) & Fun(x)] — "никакая домашка не доставляет удовольствия"; (2) Ex[Homework(x) & Reading(x)] — "некоторая домашка — чтение". Заключение: Ex[Reading(x) & ~Fun(x)] — "некоторое чтение не доставляет удовольствия".

Подсказка: Используйте правило EI и add_existential_derivation.

Задание 10.6 (Task 10.6)

Реализуйте метод add_flipped_equality(flipped, line_number), который должен добавить строки к доказательству, последняя из которых — формула flipped вида t = s, предполагая, что строка с номером line_number содержит формулу s = t.

Задание 10.7 (Task 10.7)

Реализуйте метод add_free_instantiation(instantiation, line_number, substitution_map), который должен добавить строки к доказательству, последняя из которых — формула instantiation. Формула instantiation должна получаться заменой в формуле из строки line_number свободные переменные в соответствии со словарём substitution_map. Чтобы избежать некорректных подстановок, сначала замените каждую переменную на временную новую переменную (поможет next(fresh_variable_name_generator)), а затем замените их на термы. Например, если в строке 17 стоит plus(x, y) = plus(y, x), то вызов

prover.add_free_instantiation('plus(f(y), g(x, 0)) = plus(g(x, 0), f(y))', 17, {'x': 'f(y)', 'y': 'g(x, 0)'}) 

должен добавить к доказательству строки, последняя из которых plus(f(y), g(x, 0)) = plus(g(x, 0), f(y)). Для этого сначала можено сделать замену на новые переменные, получится формула вида plus(z1,z2)=plus(z2,z1), послед этого можено спокойно заменить z1 на f(y), а z2 - на g(x, 0).

Задание 10.8 (Task 10.8)

Реализуйте метод add_substituted_equality(substituted, line_number, parametrized_term), который должен добавить строки к доказательству, последняя из которых — формула substituted. Строка line_number должна содеражить равенство вида t = s, а формула substituted должна иметь вид u(t) = u(s) — результат подстановок в параметризованной терм u(_) сначала терма t, а потом терма s.

Задание 10.9 (Task 10.9) Реализуйте метод add_chained_equality(chained, line_numbers), который, используя цепочку равенств

t1 = t2, t2 = t3, ..., t{n-1} = tn, 

содержащихся в строках с номерами line_numbers, последовательно объединяет их, чтобы в итоге вывести формулу t1 = tn. Рекомендуется реализовать вспомогательный метод _add_chaining_of_two_equalities(line_number1, line_number2).

В следующих 4 заданиях надо использовать предопределенные в файле some_proofs.py системы аксиом GROUP_AXIOMS, FIELD_AXIOMS, PEANO_AXIOMS и COMPREHENSION_AXIOM.

Задание 10.10 (Task 10.10)

Реализуйте функцию prove_group_unique_zero(), доказывающую следующее:

Посылки: аксиомы группы (GROUP_AXIOMS) и формула a + c = a

Заключение: c = 0.

Задание 10.11 (Task 10.11)

Реализуйте функцию prove_field_zero_multiplication(), доказывающую:

Посылки: аксиомы поля (FIELD_AXIOMS)

Заключение: 0 * x = 0.

Задание 10.12 (Task 10.12)

Реализуйте функцию prove_peano_left_neutral(), доказывающую:

Посылки: аксиомы Пеано (включая схему индукции) (PEANO_AXIOMS)

Заключение: 0 + x = x

Задание 10.13 (Task 10.13)

Реализуйте функцию prove_russell_paradox(), доказывающую

Посылки: схема аксиом свертывания (COMPREHENSION_AXIOM)

Заключение: противоречие z=z & ~z=z