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

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск

Объявления

Введение

Этот курс -- попытка представить математическую логику через призму программирования на 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.


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

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

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

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

Задание 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() до тех пор, пока все вхождения данной леммы не будут удалены.

Задание 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 → ψ))’ является с

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

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

Задание 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.

Задание 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.

Задание 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.

Источник — «http://wiki.cs.hse.ru/index.php?title=Математическая_логика_на_Python_25&oldid=90016»