Выводимость логических формул из аксиом

Задание 1

№	Аксиома	Время вывода
4	a*b>a	20.6837233s
5	a*b>b	3.0743ms
6	a>(b>(a*b))	49.8335958s
7	a>(a|b)	5.5473203s
8	b>(a|b)	3.1782ms
9	(a>c)>((b>c)>((a|b)>c))	29.087582s
10	!a>(a>b)	27.4935ms
11	a|!a	2.4164ms

Задание 2

Задание 3

В методе резолюций используются резольвенты:
¬B∨С A∨B ⊢ A∨C
Заметим, что ¬B∨С = B→C и A∨B = ¬A→B, используем гипотетический силлогизм и получим: ¬A→C = A∨C
Следовательно, для посылок, имеющих вид формул, включающих только импликации и отрицания, в аналоге метода резолюций можно использовать:
B→C ¬A→B ⊢ ¬A→C
В тех случаях, когда посылки имеют вид:
B→C ¬B→A или A→B C→¬B можно применить закон контрапозиции:
A→B ⟺ ¬B→¬A
Если посылка имеет вид: B, то она представима в виде: ¬B→F или T→B (F - false, T - true)

Пример

Если бы он не сказал, она бы и не узнала. Если бы она не спросила, он бы и не сказал. Она узнала, значит, сказала.
A - она спросила
B - он сказал
C - она узнала
1: ¬A→¬B 2: ¬B→¬C 3: C ⊢ A
4: ¬A
5: 1,2 ⊢ ¬A→¬C
6: 1,4 ¬A→¬B T→¬A ⊢ T→¬B или ¬B
7: 2,3 ¬B→¬C ¬C→F ⊢ ¬B→F или B
8: 6,7 T→¬B ¬B→F ⊢ T→F = F - получили противоречие

Задание 4

Проанализировав все выложенные решения и предложенные другими командами тождества, мы решили использовать в нашем выражении забытую всеми операцию XOR. На выбор представлено три аксиомы разного уровня сложности.

Аксиома	Время вывода
((!a>!b)>(c>(!a>b)))>((!a>!b)>(c>a))	9.9390967s
(((a>(a>b))>((!c>!d)>((!c>d)>c)))*e)>e	24.1775638s
(a+b)>(b+a)	>1m

Запуск

Запуск на любой платформе

1. Скачать установщик Go

Откройте сайт https://go.dev/dl/ и скачайте подходящий под вашу ОС установщик.

2. Установите Go

Проследуйте инструкциям, указанным на официальном сайте https://go.dev/doc/install.

3. Проверьте установку

Выполните в консоли (терминале) команду go version. В случае успеха, вы должны увидеть что-то подобное go version go1.23.3 windows/amd64.

4. Установите приложение

Выполните в консоли (терминале) команду go install github.com/spanwalla/logical-inference/cmd/inference@latest.

5. Запуск приложение

Выполните в консоли (терминале) из любой локации команду inference. Если всё установилось правильно, программа должна запуститься и вы сможете ввести логическое выражение.

Запуск на Windows

Вы можете воспользоваться заранее скомпилированным исполняемым файлом, который находится в разделе Releases.

Использование

Обозначения

Операция	Обозначение
Отрицание (НЕ)	!
Дизъюнкция (ИЛИ)	|
Конъюнкция (И)	*
Импликация (→)	>
Исключающее ИЛИ (XOR)	+
Эквиваленция (=)	=

Ввод формул

Формулы вводятся без пробелов, допустимо использовать круглые скобки ( ). Пример: (a>(b>c))>((a>b)>(a>c)), !a>!b.