Как составить алгоритм доказательства какого-нибудь общезначимого высказывания с помощью исчисления высказываний?

[Anatoliy.Kramko]

Как составить алгоритм доказательства какого-нибудь общезначимого высказывания с помощью исчисления высказываний?
 
Более подробно – ниже.
 
-
 
Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Например, x v !x? Можно использовать, к примеру, эту аксиоматику:
1: A -> ( B -> A)
2: (A -> -> (( A -> (B -> C)) -> (A -> C)
3: A & B -> A
4: A & B -> B
5: A -> (B -> A &
6: A -> A v B
7: B -> A v B
8: (A -> Q) -> ((B -> Q) -> (A v B ->Q))
9: (A -> -> ((A -> !B) -> !A)
10: !!A -> A
 
Я смотрю на примеры доказательств (http://mathhelpplanet.com/static.php?p=formalizovannoye-ischisleniye-vyskazyvaniyhttp://mathhelpplanet.com/static.php?p=for...ye-vyskazyvaniy - они не без помарок, но в общем понятные). Там вывод осуществляется из гипотез (которые неявно объединены в конъюнкцию), есть семантическое следование из них в доказываемое высказывание. Здесь же у нас нет гипотез, нет следования. Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как? Как конкретно доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Я пытаюсь решить (наметить план решения) третье задание следующего содержания (перепишу основную его часть):
 
«Написать программу, строящую доказательство указанного во входном файле высказывания (если оно общезначимо), либо дающую оценку пропозициональных переменных, на которых высказывание ложно (если оно опровержимо).
Входной файл состоит из единственной строки, содержащей формулу исчисления высказываний, которую требуется доказать или опровергнуть. Высказывание удовлетворяет грамматике из первого задания. Выходной файл должен либо содержать доказательство высказывания (в формате доказательства из первого задания)…»
 
Первое задание (тоже не очень понятно как решать) задаёт грамматику формами Бэкуса-Наура и его основная часть звучит следующим образом:
 
«Написать программу, проверяющую доказательства в исчислении высказываний на корректность. Входной файл представляет из себя последовательность высказываний, по высказыванию на строку. ... Результатом работы программы должен быть проаннотированный текст доказательства, касательно каждой строки должно быть указано, из чего и как она получается.»

[folk]

слайд 6
http://iamdrunk.ru/teach/%D0%A3%D1%87%D0%B...8%D1%8F%203.ppt
 

[Anatoliy.Kramko]

Source of the post слайд 6

 
Прекрасный пример. Я таких примеров видел много, даже дал ссылку на них в начальном сообщении. Как составить УНИВЕРСАЛЬНЫЙ алгоритм подобных действий (а то даже "на бумаге" я действую в основном наугад - я уж не говорю о составлении компьютерной программы)?

[folk]

Универсального "алгоритма" не существует. Ибо проблема алгоритмически неразрешима. Реально работающие варианты (подходы) - HOL 88 там неплохая документация и как часть системы есть модуль доказывающий автоматически теоремы логики первого порядка (эвристический перебор правил вывода). И Mizar (резолюция). Обе системы большие и непростые.
Если вам надо что то простенькое - то можно взять за основу подход HOL 88 он основан на строгой типизации в SML но может быть реализован в любом языке. Пишете абстрактный тип данных соответствующий правильно построенным формулам и выводам и шарашите полный перебор. На каждом шаге можно оглядеться и оценить некую дальность от результата, количество гипотез и так далее.
Но в реальной жизни конечно от аксиом никто не доказывают - работают либо по таблицам истинности либо в стиле м одель чекеров - но вам как я понял надо именно аксиоматическое доказательство. Снимаю шляпу. По указанным ключевым словам наверняка найдете несколько статей с описанием алгоритмов)
 

[folk]

по первому заданию как мне кажется проверка высказывания по всем переменным дает возможность привести контрпример, если же его нет то пруф (в общем подход модель чекеров должен вас устроить)
по второму - если между формулами переход ровно по одному правилу вывода то это вполне решаемо - у вас есть абстрактное дерево для ф1 и для ф2 и некий образец (дерево с подстановками в некие вершины) и вам надо понять как в образец подставить ф1 чтобы получилось ф2 - в общем то обычная унификация - есть много статей на эту тему. Ну и перебор по правилам. В теории можно было бы унифицировать сами ф1 и ф2 а потом сравнить с правилами - но мне кажется это трудно

[Anatoliy.Kramko]

Source of the post Универсального "алгоритма" не существует. Ибо проблема алгоритмически неразрешима. Реально работающие варианты (подходы) - HOL 88 там неплохая документация и как часть системы есть модуль доказывающий автоматически теоремы логики первого порядка (эвристический перебор правил вывода). И Mizar (резолюция). Обе системы большие и непростые.
Если вам надо что то простенькое - то можно взять за основу подход HOL 88 он основан на строгой типизации в SML но может быть реализован в любом языке. Пишете абстрактный тип данных соответствующий правильно построенным формулам и выводам и шарашите полный перебор. На каждом шаге можно оглядеться и оценить некую дальность от результата, количество гипотез и так далее.
Но в реальной жизни конечно от аксиом никто не доказывают - работают либо по таблицам истинности либо в стиле м одель чекеров - но вам как я понял надо именно аксиоматическое доказательство. Снимаю шляпу. По указанным ключевым словам наверняка найдете несколько статей с описанием алгоритмов)

 
Это малая часть домашнего задания для третьего семестра петербургского вуза ИТМО (прилагаю файл, задача 3). Да, мне нужно от аксиом. Я уже cпрашивал об этом на форумах, объяснили, что нужно как-то доказать для каждой строки таблицы истинности путём разбивки на операции, а дальше слепить строки в одно. Как-то так.
Да, легче методом резолюций, по таблице истинности или как-то ещё. Но мне надо от аксиом, самому. На то это и исчисление высказываний.
SML мне не подходит, нужен С++.
Очень хотелось бы у вас узнать - почему вы думаете, что проблема алгоритмически неразрешима? 
Спасибо за ключевые слова.
 




[img]/modules/file/icons/application-pdf.png[/img] ДЗ по матлогике.pdf

[Anatoliy.Kramko]

Source of the post
по первому заданию как мне кажется проверка высказывания по всем переменным дает возможность привести контрпример, если же его нет то пруф (в общем подход модель чекеров должен вас устроить)

по второму - если между формулами переход ровно по одному правилу вывода то это вполне решаемо - у вас есть абстрактное дерево для ф1 и для ф2 и некий образец (дерево с подстановками в некие вершины) и вам надо понять как в образец подставить ф1 чтобы получилось ф2 - в общем то обычная унификация - есть много статей на эту тему. Ну и перебор по правилам. В теории можно было бы унифицировать сами ф1 и ф2 а потом сравнить с правилами - но мне кажется это трудно

По певому заданию я пытаюсь сделать бинарное дерево или ПОЛИЗ, чтобы проверить по всем переменным (без контрпримера). По второму - смотрю на доказательство теоремы дедукции и думаю.

[folk]

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