Математическая логика на Python 25 — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(Добавлено ДЗ №2)
Строка 31: Строка 31:
 
Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2
 
Загрузить можно в гугл классе: https://classroom.google.com/c/NzI1NTIzNTE3MjA0?cjc=frttno2
  
==== Задание 1.1 (Task 1.1)====
+
<big>Задание 1.1 (Task 1.1)</big>
 
В файле мето отмечено следующим комментарием: # Task 1.1
 
В файле мето отмечено следующим комментарием: # Task 1.1
  
Строка 38: Строка 38:
 
Обратите внимание, что в Python строка, возвращаемая методом formula.__repr__(), также возвращается вызовом str(formula). Таким образом, решив эту задачу, вы также реализуете функциональность метода str() для данного класса.
 
Обратите внимание, что в Python строка, возвращаемая методом formula.__repr__(), также возвращается вызовом str(formula). Таким образом, решив эту задачу, вы также реализуете функциональность метода str() для данного класса.
  
==== Задание 1.2 (Task 1.2) ====
+
<big>Задание 1.2 (Task 1.2)</big>
 
Реализуйте недостающий код для метода variables() класса Formula, который возвращает множество (set) имен переменных, присутствующие в формуле. Напомним, что имя переменной — это лист дерева, метка которого является буквой от «p» до «z», за которой следуют цифры.
 
Реализуйте недостающий код для метода variables() класса Formula, который возвращает множество (set) имен переменных, присутствующие в формуле. Напомним, что имя переменной — это лист дерева, метка которого является буквой от «p» до «z», за которой следуют цифры.
  
==== Задание 1.3 (Task 1.3) ====
+
<big>Задание 1.3 (Task 1.3)</big>
  
 
Реализуйте недостающий код для метода operators() класса Formula, который возвращает все операторы, присутствующие в формуле. Операторами в этом задании являются не только все унарные и бинарные операторы, но и константы T и F.
 
Реализуйте недостающий код для метода operators() класса Formula, который возвращает все операторы, присутствующие в формуле. Операторами в этом задании являются не только все унарные и бинарные операторы, но и константы T и F.
  
==== Задание 1.4 (Task 1.4)====
+
<big>Задание 1.4 (Task 1.4)</big>
  
 
Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, и возвращает формулу (объект типа Formula), созданное из префикса строки, а также строку, содержащую непроанализированный остаток строки (которая может быть пустой, если вся строка образует формулу). Обратите внимание, что формула это очень строгое формальное понятие, обратите внимание на скобки.
 
Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, и возвращает формулу (объект типа Formula), созданное из префикса строки, а также строку, содержащую непроанализированный остаток строки (которая может быть пустой, если вся строка образует формулу). Обратите внимание, что формула это очень строгое формальное понятие, обратите внимание на скобки.
  
==== Задание 1.5 (Task 1.5)====
+
<big>Задание 1.5 (Task 1.5)</big>
  
 
Реализуйте недостающий код для статичного метода is_formula(string) класса Formula, который проверяет, представляет ли заданная строка корректную формулу.
 
Реализуйте недостающий код для статичного метода is_formula(string) класса Formula, который проверяет, представляет ли заданная строка корректную формулу.
Строка 55: Строка 55:
 
Подсказка: используйте метод _parse_prefix().
 
Подсказка: используйте метод _parse_prefix().
  
==== Задание 1.6 (Task 1.6)====
+
<big>Задание 1.6 (Task 1.6)</big>
  
 
Реализуйте недостающий код для статичного метода parse(string) класса Formula, который разбирает строковое представление формулы. (Можно предположить, что входная строка корректна, то есть удовлетворяет предусловию Formula.is_formula(string), в коде уже есть соответствующий assert)
 
Реализуйте недостающий код для статичного метода parse(string) класса Formula, который разбирает строковое представление формулы. (Можно предположить, что входная строка корректна, то есть удовлетворяет предусловию Formula.is_formula(string), в коде уже есть соответствующий assert)
  
 
Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter01.py
 
Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл 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

Версия 05:41, 30 января 2025

Объявления

Введение

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