Математическая логика на Python - История изменений

Ekononova: /* Объявления */ ДЗ11

2026-06-16T01:19:35Z

Объявления: ДЗ11

← Предыдущая версия		Версия от 01:19, 16 июня 2026
Строка 10:		Строка 10:
	* Появилось описание ДЗ№9 (дэдлайн 20.05.26)		* Появилось описание ДЗ№9 (дэдлайн 20.05.26)
	* Появилось описание ДЗ№10 (дэдлайн 04.06.26)		* Появилось описание ДЗ№10 (дэдлайн 04.06.26)
			* Появилось описание ДЗ№11 (дедлайн 18.06.26)

	== Введение ==		== Введение ==

Ekononova: /* Домашнее задание №11 (дедлайн 18.06.26) */

2026-06-16T01:18:09Z

Домашнее задание №11 (дедлайн 18.06.26)

← Предыдущая версия		Версия от 01:18, 16 июня 2026
Строка 743:		Строка 743:

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

			===Домашнее задание №11 (дедлайн 18.06.26)===

			В этом задании вам предстоит реализовать несколько методов в разных файлах. Файлы будут указываться в каждом задании. Это последнее домашнее задание, оно посвящено подготовке к доказательству теоремы о полноте для исчисления предикатов.

			<big>Задание 11.1 (Task 11.1) (file:predicates/deduction.py)</big>

			Реализуйте недостающий код для функции remove_assumption(proof, assumption). Эта функция принимает на вход вывод некоторого заключения ψ, которое:

			- вывод (proof) имеет среди посылок наши шесть схем логических аксиом логики предикатов,
			- вывод также имеет данную формулу φ (assumption), как простую формулу (не схему, т.е. без шаблонов),
			- вывод не использует правило UG (введение квантора всеобщности) ни по какой переменной, которая свободна в φ.

			Функция возвращает доказательство формулы (φ → ψ) из тех же формул, за исключением φ.

			Подсказки: как в главе 5, для каждой формулы α, выводимой в некоторой строке исходного доказательства, новое доказательство должно выводить (φ → α); то есть предлагаемая стратегия заключается в том, чтобы построить ваше доказательство, просматривая строки данного доказательства по порядку, и всякий раз, когда строка исходного доказательства выводит некоторую α, добавлять одну или несколько строк в новое доказательство, которые в совокупности выводят (φ → α). Смело используйте тавтологическии. Когда исходная строка доказательства использует UG, вам придется потрудиться немного больше — попытайтесь понять, как в этом случае использовать аксиому US.

			<big>Задание 11.2 (Task 11.2) (file:predicates/deduction.py)</big>

			Реализуйте недостающий код для функции prove_by_way_of_contradiction(proof, assumption). Эта функция принимает на вход вывод (proof) некоторого противоречия, такое что:

			- вывод имеет среди своих посылок наши шесть схем логических аксиом,
			- вывод имеет данное допущение φ (assumption) как простая формула (без шаблонов),
			- вывод не использует правило UG ни по какой переменной, которая свободна в φ.

			Функция возвращает доказательство формулы ~φ из тех же посылок, за исключением φ.

			Рекомендации: Помните, что объекты Proof неизменяемы (immutable). Поэтому вы не можете просто добавлять строки к какому-либо объекту Proof. Вместо этого создайте новый объект Prover, используйте его метод add_proof() (который уже реализован для вас), чтобы вставить все строки любого объекта Proof в доказательство этого prover'а, а затем добавьте больше строк в это доказательство с помощью API Prover, включая методы, которые вы реализовали в главе 10 (и, в частности, add_tautological_implication()).

			<big>Задание 11.3 (Task 11.3) (file:predicates/prenex.py)</big>

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

			Рекомендации: Сначала реализуйте недостающий код для рекурсивной функции is_quantifier_free(formula), которая проверяет, не содержит ли данная формула кванторов, а затем используйте эту функцию для решения исходной задачи.

			<big>Задание 12.1 (Task 12.1) (file: predicates/completeness.py)</big>

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

			a. Реализуйте недостающий код для функции `is_primitively_closed(sentences)`, которая возвращает, является ли данное (конечное) множество предложений в предваренной нормальной форме примитивно замкнутым.

			Опр. Множество формул в предваренной нормальной форме S называется примитивно замкнутым, если для каждого имени отношения R, которое встречается где-либо в S, и для каждого кортежа (не обязательно различных) имён констант c1,…,cn, где n — арность R и каждое ci встречается где-либо в S, либо примитивное предложение R(c1,…,cn), либо его отрицание ∼R(c1,…,cn) (или оба) находится в S.

			Подсказка: может быть полезен метод relations() класса Formula, а также метод product() (с его аргументом repeat) из стандартного модуля Python itertools.

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

			Опр. S - универсально замкнуто, если для каждого универсально квантифицированного предложения ∀x[φ(x)] в S и каждого имени константы c, которое встречается где-либо в S, универсальная конкретизация φ(c) также лежит в S.

			Подсказка: может быть полезен метод substitute() класса Formula.

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

			Опр. S - экзистенциально замкнуто, елси для каждого экзистенциально квантифицированного предложения ∃x[φ(x)] в S существует такое имя константы c, что экзистенциальный свидетель φ(c) этой формулы также лежит в S.

			Подсказка: метод substitute() класса Formula также может быть здесь полезен.

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

			Реализуйте недостающий код для функции find_unsatisfied_quantifier_free_sentence(sentences, model, unsatisfied), которая принимает универсально и экзистенциально замкнутое (конечное) множество предложений в пренексной нормальной форме sentences, принимает модель model, универсум которой состоит из множества имён констант, встречающихся где-либо в sentences, и принимает предложение unsatisfied (которое может содержать кванторы) из sentences, ложное в модели, и возвращает бескванторное предложение из sentences, ложное в модели. Чтобы проверить, что вы действительно используете условия универсальной и экзистенциальной замкнутости в вашем решении (а не просто перебираете предложения, пока не найдёте подходящее для возврата), тесты для этого задания реализованы таким образом, что «множество» sentences, передаваемое этой функции, на самом деле не поддерживает итерацию. Вместо этого к нему можно обращаться только с помощью запросов на принадлежность, то есть с помощью оператора Python `in`: например, if sentence in sentences. (В терминологии Python параметр sentences является контейнером (Container), но не абстрактным множеством (AbstractSet).)

			Подсказка: используйте рекурсию, чтобы «снимать» по одному квантору за раз (заменяя связанную переменную на некоторое имя константы), сохраняя при этом условие, что результирующее предложение находится в данном множестве предложений и не удовлетворяется данной моделью. Используйте тот факт, что данное множество предложений является универсально и экзистенциально замкнутым, чтобы направлять вашу реализацию и обеспечивать её корректность.

Ekononova в 16:06, 25 мая 2026

2026-05-25T16:06:00Z

← Предыдущая версия		Версия от 16:06, 25 мая 2026
Строка 9:		Строка 9:
	* Дэдлайн ДЗ№8 перенесен на 05.05.26		* Дэдлайн ДЗ№8 перенесен на 05.05.26
	* Появилось описание ДЗ№9 (дэдлайн 20.05.26)		* Появилось описание ДЗ№9 (дэдлайн 20.05.26)
			* Появилось описание ДЗ№10 (дэдлайн 04.06.26)

	== Введение ==		== Введение ==

Ekononova: ДЗ №10

2026-05-25T16:05:10Z

ДЗ №10

← Предыдущая версия		Версия от 16:05, 25 мая 2026
Строка 638:		Строка 638:
	– Используйте `prove_propositional_tautology()` (импортирована из `propositions.tautology`).		– Используйте `prove_propositional_tautology()` (импортирована из `propositions.tautology`).
	– Затем примените вашу функцию `_prove_from_skeleton_proof`.		– Затем примените вашу функцию `_prove_from_skeleton_proof`.

			===Домашнее задание №10 (дедлайн 04.06.26)===

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

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

			Реализуйте метод 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))).

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

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

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

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

			Подсказка: вспомните задание №6.4, в котором реализовывался метод prove_sound_inference().

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

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

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

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

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

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

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

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

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

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

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

			Реализуйте метод 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).

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

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

			<big>Задание 10.9 (Task 10.9)</big> Реализуйте метод 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ekononova: опечатки

2026-05-14T12:10:02Z

опечатки

← Предыдущая версия		Версия от 12:10, 14 мая 2026
Строка 41:		Строка 41:
	* В пайплайнах гитхаба можете видеть бинарную оценку за каждый тест для данной дз.		* В пайплайнах гитхаба можете видеть бинарную оценку за каждый тест для данной дз.

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

	В этом задании вам надо будет внести изменения в файл propositions/syntax.py		В этом задании вам надо будет внести изменения в файл propositions/syntax.py
Строка 83:		Строка 83:
	Нужно реализовать статический метод parse_polish(string) класса Formula. Метод парсит строку в формулу. Строка представляет собой запись формулы в польской нотации.		Нужно реализовать статический метод parse_polish(string) класса Formula. Метод парсит строку в формулу. Строка представляет собой запись формулы в польской нотации.

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

	В этом задании вам надо будет внести изменения в файл propositions/semantics.py		В этом задании вам надо будет внести изменения в файл propositions/semantics.py
Строка 118:		Строка 118:
	Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter02.py		Чтобы проверить верно ли вы сделали все задание надо в корне папки запустить файл test_chapter02.py

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

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

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

	<big>Задание 1 (Task 4.1)</big>		<big>Задание 1 (Task 4.1)</big>
Строка 282:		Строка 282:
	Каждое задание проверяйте на корректность с помощью тестов в файле test_chapter04.py.		Каждое задание проверяйте на корректность с помощью тестов в файле test_chapter04.py.

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

	<big>Задание 5.1 (Task 5.1)</big> file:propositions/proofs.py		<big>Задание 5.1 (Task 5.1)</big> file:propositions/proofs.py
Строка 333:		Строка 333:
	'''Подсказка:''' Используйте теорему о дедукции (remove_assumption(proof)) и затем аксиому N.		'''Подсказка:''' Используйте теорему о дедукции (remove_assumption(proof)) и затем аксиому N.

	=== Домашнее задание №5-bis (~~дэдлайн~~ 17.03.26)===		=== Домашнее задание №5-bis (дедлайн 17.03.26)===
	Суть этого задания состоит в том, чтобы потренироваться в создании доказательство (выводов), но не непосредственно, а с помощью уже написанных методов. Например, чтобы построить вывод формулы p->p		Суть этого задания состоит в том, чтобы потренироваться в создании доказательство (выводов), но не непосредственно, а с помощью уже написанных методов. Например, чтобы построить вывод формулы p->p
	можно вызвать метод remove_assumption(...) подав на вход вывод состоящий из одной формулы p. На выходе вы получите более длинный вывод, который, при необходимости, можно дальше использовать.		можно вызвать метод remove_assumption(...) подав на вход вывод состоящий из одной формулы p. На выходе вы получите более длинный вывод, который, при необходимости, можно дальше использовать.
Строка 354:		Строка 354:
	Смысл этого состоит в том, что мы можем заменить N на N' и при этом не поменяется множество выводимых формул.		Смысл этого состоит в том, что мы можем заменить N на N' и при этом не поменяется множество выводимых формул.

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

	<big>Задание 6.1 (Task 6.1)</big> (file: propositions/tautology.py)		<big>Задание 6.1 (Task 6.1)</big> (file: propositions/tautology.py)
Строка 404:		Строка 404:
	Постарайтесь осознать, как код который вы пишите повторяет доказательства, которые были на лекциях.		Постарайтесь осознать, как код который вы пишите повторяет доказательства, которые были на лекциях.

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

	<big>Задание 7.1 (Task 7.1)</big> (file: predicates/syntax.py)		<big>Задание 7.1 (Task 7.1)</big> (file: predicates/syntax.py)
Строка 448:		Строка 448:
	Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.		Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.

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

	<big>Задание 8.1 (Task 8.1)</big> (file: predicates/functions.py)		<big>Задание 8.1 (Task 8.1)</big> (file: predicates/functions.py)
Строка 486:		Строка 486:
	'''Требование:''' Для любой модели model и формул new_formulas=replace_equality_with_SAME_in_formulas(formulas) должно выполняться: model является моделью new_formulas тогда и только тогда, когда make_equality_as_SAME_in_model(model) является моделью formulas.		'''Требование:''' Для любой модели model и формул new_formulas=replace_equality_with_SAME_in_formulas(formulas) должно выполняться: model является моделью new_formulas тогда и только тогда, когда make_equality_as_SAME_in_model(model) является моделью formulas.

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

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

Ekononova: опечатка

2026-05-14T12:02:26Z

опечатка

← Предыдущая версия		Версия от 12:02, 14 мая 2026
Строка 48:		Строка 48:

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

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

Ekononova: ДЗ №9

2026-05-11T12:57:03Z

ДЗ №9

← Предыдущая версия		Версия от 12:57, 11 мая 2026
Строка 8:		Строка 8:
	* Появилось описание ДЗ№8 (изм. дэдлайн 05.05.26)		* Появилось описание ДЗ№8 (изм. дэдлайн 05.05.26)
	* Дэдлайн ДЗ№8 перенесен на 05.05.26		* Дэдлайн ДЗ№8 перенесен на 05.05.26
			* Появилось описание ДЗ№9 (дэдлайн 20.05.26)

	== Введение ==		== Введение ==

Ekononova: /* Домашнее задание №9 (дэдлайн 20.05.25) */

2026-05-11T12:56:08Z

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

Внесённые изменения

Ekononova в 12:20, 11 мая 2026

2026-05-11T12:20:11Z

← Предыдущая версия		Версия от 12:20, 11 мая 2026
Строка 6:		Строка 6:
	* Появилось описание ДЗ№6 (Дэдлайн 24.03.26)		* Появилось описание ДЗ№6 (Дэдлайн 24.03.26)
	* Появилось описание ДЗ№7 (дэдлайн 13.04.26)		* Появилось описание ДЗ№7 (дэдлайн 13.04.26)
	* Появилось описание ДЗ№8 (дэдлайн 28.04.26)		* Появилось описание ДЗ№8 (изм. дэдлайн 05.05.26)
			* Дэдлайн ДЗ№8 перенесен на 05.05.26

	== Введение ==		== Введение ==

Ekononova: дэдлайн изменен

2026-05-11T12:19:04Z

дэдлайн изменен

← Предыдущая версия		Версия от 12:19, 11 мая 2026
Строка 446:		Строка 446:
	Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.		Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.

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

	<big>Задание 8.1 (Task 8.1)</big> (file: predicates/functions.py)		<big>Задание 8.1 (Task 8.1)</big> (file: predicates/functions.py)