Просмотр исходного текста страницы Математическая логика на 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

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

=== Описание курса ===
Курс включает пропозициональную логику и логику первого порядка. При этом планируется логику планируется изложить на уровне полноценного курса по математической логики со всеми важными теоремами и доказательствами. В качестве литературы можно использовать [https://old.mccme.ru//free-books//shen/shen-logic-part2-5ed.pdf Н. К. Верещагин, А. Шень. Часть 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

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

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

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

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

<big>Задание 1.3 (Task 1.3)</big>

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

<big>Задание 1.4 (Task 1.4)</big>

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

<big>Задание 1.5 (Task 1.5)</big>

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

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

<big>Задание 1.6 (Task 1.6)</big>

Реализуйте недостающий код для статичного метода 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

<big>Задание 2.1 (Task 2.1)</big>

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

<big>Задание 2.2 (Task 2.2)</big>

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

<big>Задание 2.3 (Task 2.3)</big>

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

<big>Задание 2.4 (Task 2.4)</big>

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

<big>Задание 2.5 (Task 2.5a, Task 2.5b, Task 2.5c)</big>

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

<big>Задание 2.6 (Task 2.6)</big>

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

<big>Задание 2.7 (Task 2.7)</big>

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

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

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

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

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

<big>Задание 1 (Task 3.1)</big>  

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

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


<big>Задание 2 (Task 3.2)</big>  

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

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

<big>Задание 3 (Task 3.3)</big>  

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

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

<big>Задание 4 (Task 3.4)</big>  

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

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

<big>Задание 5 (Task 3.5)</big>  

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

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

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

* to_not_and(formula)  
* to_nand(formula)  
* to_implies_not(formula)  
* to_implies_false(formula)  

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

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

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

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

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

---

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

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

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

---

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

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

---

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

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

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

---

<big>Задание 5 (Task 4.5)</big>  
Файл: 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.  

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

--- 

<big>Задание 6 (Task 4.6)</big>  
Файл: 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 логически следует из Г.

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


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

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

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

---

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

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

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

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

---

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

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

---

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

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

---

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


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

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

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

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

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

<big>Задание 3 (Task 5.3)</big>  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 → ψ))’ является с

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

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

<big>Задание 5 (Task 5.5)</big>  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.

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

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

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

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

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

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