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

Ekononova в 11:25, 12 июня 2025

2025-06-12T11:25:00Z

← Предыдущая версия		Версия от 11:25, 12 июня 2025
Строка 10:		Строка 10:
	* Добавлено ДЗ №7 Дэдлайн - 25.04.25		* Добавлено ДЗ №7 Дэдлайн - 25.04.25
	* Добавлено ДЗ №8 Дэдлайн - 16.05.25		* Добавлено ДЗ №8 Дэдлайн - 16.05.25
	* Добавлено ДЗ №9 Дэдлайн - 30.05.25		* Добавлено ДЗ №9 Дэдлайн - 06.06.25
			* Добавлено ДЗ №10 Дэдлайн - 19.06.25

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

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

2025-06-12T11:24:24Z

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

← Предыдущая версия		Версия от 11:24, 12 июня 2025
Строка 459:		Строка 459:
	'''Требование:''' Для любой модели 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 (дэдлайн 30.05.25)===		===Домашнее задание №9 (дэдлайн 06.06.25)===

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

Ekononova в 11:23, 12 июня 2025

2025-06-12T11:23:40Z

← Предыдущая версия		Версия от 11:23, 12 июня 2025
Строка 612:		Строка 612:
	– Затем примените вашу функцию `_prove_from_skeleton_proof`.		– Затем примените вашу функцию `_prove_from_skeleton_proof`.

	===Домашнее задание №10 (дэдлайн — 19 ~~июня~~)===		===Домашнее задание №10 (дэдлайн — 19.06.25)===

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

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

2025-06-12T11:23:08Z

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

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

			===Домашнее задание №10 (дэдлайн — 19 июня)===

			В этом задании вам предстоит реализовать недостающие методы класса 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

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

			Подсказка: вспомните задачу №4 в домашнем задании №6, котором реализовался метод 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 в 00:52, 23 мая 2025

2025-05-23T00:52:09Z

← Предыдущая версия		Версия от 00:52, 23 мая 2025
Строка 10:		Строка 10:
	* Добавлено ДЗ №7 Дэдлайн - 25.04.25		* Добавлено ДЗ №7 Дэдлайн - 25.04.25
	* Добавлено ДЗ №8 Дэдлайн - 16.05.25		* Добавлено ДЗ №8 Дэдлайн - 16.05.25
			* Добавлено ДЗ №9 Дэдлайн - 30.05.25

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

Ekononova в 00:51, 23 мая 2025

2025-05-23T00:51:27Z

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

Ekononova в 12:22, 2 мая 2025

2025-05-02T12:22:40Z

← Предыдущая версия		Версия от 12:22, 2 мая 2025
Строка 9:		Строка 9:
	* Добавлено ДЗ №6 Дэдлайн - 28.03.25		* Добавлено ДЗ №6 Дэдлайн - 28.03.25
	* Добавлено ДЗ №7 Дэдлайн - 25.04.25		* Добавлено ДЗ №7 Дэдлайн - 25.04.25
			* Добавлено ДЗ №8 Дэдлайн - 16.05.25

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

Ekononova: ДЗ №8

2025-05-02T12:21:26Z

ДЗ №8

@@ Строка 394: / Строка 394: @@
 a. Реализуйте недостающий код для статического метода _parse_prefix(string) класса Formula, который принимает строку, содержащую префикс, представляющий формулу, и возвращает объект типа Formula и оставшуюся неразобранную часть строки.
 b. Реализуйте недостающий код для статического метода parse(string) класса Formula, который разбирает строковое представление формулы. Можно считать, что входная строка представляет корректную формулу.
@@ Строка 416: / Строка 418: @@
 Реализуйте недостающий код для метода is_model_of(formulas) класса Model, который проверяет, является ли данная модель моделью всех данных формул при любом назначении свободных переменных.

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

2025-04-14T18:54:31Z

Объявления

← Предыдущая версия		Версия от 18:54, 14 апреля 2025
Строка 8:		Строка 8:
	* Добавлено ДЗ №5 Дэдлайн - 14.03.25		* Добавлено ДЗ №5 Дэдлайн - 14.03.25
	* Добавлено ДЗ №6 Дэдлайн - 28.03.25		* Добавлено ДЗ №6 Дэдлайн - 28.03.25
			* Добавлено ДЗ №7 Дэдлайн - 25.04.25

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

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

2025-04-14T18:54:00Z

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

← Предыдущая версия		Версия от 18:54, 14 апреля 2025
Строка 373:		Строка 373:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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